Theorems · Theorem · ring theory
IsDomain.of_faithfulSMul
∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [FaithfulSMul R A] [IsDomain A], IsDomain R
- Defined in
- Mathlib.Algebra.Algebra.Basic
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 22 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- Algebrastatement and proof · cited by 11,388
- CommSemiringstatement and proof · cited by 10,911
- Algebra.algebraMapproof · cited by 4,706
- IsDomainstatement and proof · cited by 2,196
- FaithfulSMulstatement and proof · cited by 340
- FaithfulSMul.algebraMap_injectiveproof · cited by 198
- Function.Injective.isDomainproof · cited by 27
Cited by10
Results whose statement or proof uses this declaration.
- IsGaloisGroup.card_eq_finrank'proof · cited by 2
- isFractionRing_of_exists_eq_algebraMap_or_inv_eq_algebraMap_of_injectiveproof · cited by 2
- IsLocalRing.primesOverFinset_eqproof · cited by 1
- IsLocalRing.primesOver_eqproof · cited by 1
- IsAlmostIntegral.isIntegralproof · cited by 1
- IsGaloisGroup.algebraMap_restrictHom_smulproof · cited by 1
- linearIndependent_algebraMap_comp_iffproof · cited by 1
- Algebra.IsAlgebraic.rank_fractionRing_mvPolynomialproof · cited by 0
- Algebra.IsAlgebraic.rank_fractionRing_polynomialproof · cited by 0
- FractionRing.algebraMap_liftAlgebrastatement · cited by 0