Theorems · Theorem · commutative algebra
nonZeroDivisors_le_comap_nonZeroDivisors_of_injective
∀ {F : Type u_1} {M₀ : Type u_2} {M₀' : Type u_3} [inst : MonoidWithZero M₀] [inst_1 : MonoidWithZero M₀']
[inst_2 : FunLike F M₀ M₀'] [NoZeroDivisors M₀'] [inst_4 : MonoidWithZeroHomClass F M₀ M₀'] (f : F),
Function.Injective ⇑f → nonZeroDivisors M₀ ≤ Submonoid.comap f (nonZeroDivisors M₀')- Cited by
- 7 results in Mathlib
- Foundations
- Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
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
- Submonoidstatement · cited by 3,086
- FunLikestatement and proof · cited by 2,560
- le_rflproof · cited by 1,558
- nonZeroDivisorsstatement and proof · cited by 895
- NoZeroDivisorsstatement and proof · cited by 545
- MonoidWithZerostatement and proof · cited by 456
- Submonoid.comapstatement · cited by 179
- MonoidWithZeroHomClassstatement and proof · cited by 37
- map_le_nonZeroDivisors_of_injectiveproof · cited by 5
- Submonoid.le_comap_of_map_leproof · cited by 3
Cited by7
Results whose statement or proof uses this declaration.
- Algebra.trace_quotient_eq_of_isDedekindDomainproof · cited by 3
- Ideal.spanIntNorm_localizationproof · cited by 3
- RatFunc.liftMonoidWithZeroHom_injectivestatement · cited by 2
- FractionalIdeal.dual_eq_dual_mul_dualproof · cited by 1
- RatFunc.liftRingHom_injectivestatement and proof · cited by 0
- RatFunc.liftAlgHom_injectivestatement and proof · cited by 0
- Module.IsTorsionFree.of_isLocalizationproof · cited by 0