Theorems · Inductive type · commutative algebra
Algebra.IsEpi
(R : Type u_1) → (A : Type u_2) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [Algebra R A] → Prop
A commutative R-algebra A is epi, if the multiplication map A ⊗[R] A → A is injective.
- Defined in
- Mathlib.Algebra.Algebra.Epi
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- CommSemiringSemiringAlgebra
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement · cited by 13,802
- Algebrastatement · cited by 11,388
- CommSemiringstatement · cited by 10,911
Cited by23
Results whose statement or proof uses this declaration.
- Algebra.isEpi_iff_forall_one_tmul_eqstatement and proof · cited by 3
- TensorProduct.lid'statement and proof · cited by 3
- Algebra.isEpi_iff_surjective_algebraMap_of_finitestatement and proof · cited by 2
- Submodule.tensorEquivSpanstatement and proof · cited by 2
- CommRingCat.epi_iff_epistatement · cited by 2
- Algebra.IsEpi.injective_lift_mulstatement and proof · cited by 1
- Algebra.isEpi_of_surjective_algebraMapstatement · cited by 1
- Submodule.tensorSpanEquivSpanstatement and proof · cited by 1
- Submodule.finrank_span_eq_finrankstatement and proof · cited by 1
- Submodule.finrank_span_eq_finrank_spanstatement and proof · cited by 1
- Algebra.injective_lift_lsmulstatement and proof · cited by 1
- Algebra.tmul_commstatement and proof · cited by 1