Theorems · Theorem · ring theory
Algebra.TensorProduct.map_bijective
∀ {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [inst : CommSemiring R] [inst_1 : Semiring A]
[inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
[inst_7 : Semiring D] [inst_8 : Algebra R D] {f : A →ₐ[R] B} {g : C →ₐ[R] D},
Function.Bijective ⇑f → Function.Bijective ⇑g → Function.Bijective ⇑(Algebra.TensorProduct.map f g)- Defined in
- Mathlib.RingTheory.TensorProduct.Maps
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Semiringstatement and proof · cited by 13,802
- Algebrastatement and proof · cited by 11,388
- CommSemiringstatement and proof · cited by 10,911
- AlgHomstatement and proof · cited by 3,236
- TensorProductstatement · cited by 2,545
- Function.Bijectivestatement and proof · cited by 863
- Algebra.TensorProduct.mapstatement · cited by 97
- TensorProduct.map_bijectiveproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- Algebra.TensorProduct.includeLeft_bijectiveproof · cited by 2