English
If h is a MulEquivClass (an equivalence induced map) between monoids with zero, then mapping the set of nonzero divisors is preserved: Submonoid.map h (nonZeroDivisors M0) = nonZeroDivisors S.
Русский
Если h — эквивалентное отображение между мономиями с нулём, то картина ненулевых делителей сохраняется: map h(nonZeroDivisors M0) = nonZeroDivisors S.
LaTeX
$$MulEquivClass.map_nonZeroDivisors (h) : Submonoid.map h (nonZeroDivisors M_0) = nonZeroDivisors S$$
Lean4
theorem map_nonZeroDivisors {M₀ S F : Type*} [MonoidWithZero M₀] [MonoidWithZero S] [EquivLike F M₀ S]
[MulEquivClass F M₀ S] (h : F) : Submonoid.map h (nonZeroDivisors M₀) = nonZeroDivisors S :=
by
let h : M₀ ≃* S := h
change Submonoid.map h _ = _
ext
simp_rw [Submonoid.map_equiv_eq_comap_symm, Submonoid.mem_comap, mem_nonZeroDivisors_iff, ← h.symm.forall_congr_right,
h.symm.toEquiv_eq_coe, h.symm.coe_toEquiv, ← map_mul, map_eq_zero_iff _ h.symm.injective]
