Theorems · Theorem · commutative algebra
map_mem_nonZeroDivisors
∀ {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₀'] [Nontrivial M₀] [NoZeroDivisors M₀'] [ZeroHomClass F M₀ M₀'] (g : F),
Function.Injective ⇑g → ∀ {x : M₀}, x ∈ nonZeroDivisors M₀ → g x ∈ nonZeroDivisors M₀'- Cited by
- 1 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext, 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
- Nontrivialstatement and proof · cited by 2,416
- nonZeroDivisorsstatement and proof · cited by 895
- NoZeroDivisorsstatement and proof · cited by 545
- MonoidWithZerostatement and proof · cited by 456
- ZeroHomClassstatement and proof · cited by 74
- eq_zero_of_ne_zero_of_mul_left_eq_zeroproof · cited by 7
- eq_zero_of_ne_zero_of_mul_right_eq_zeroproof · cited by 7
- map_ne_zero_of_mem_nonZeroDivisorsproof · cited by 6
Cited by1
Results whose statement or proof uses this declaration.
- IsFractionRing.ideal_span_singleton_map_subsetproof · cited by 1