Function.Injective.noZeroDivisors

theorem Function.Injective.noZeroDivisors : ∀ {M₀ : Type u_1} {M₀' : Type u_3} [inst : Mul M₀] [inst_1 : Zero M₀] [inst_2 : Mul M₀'] [inst_3 : Zero M₀'] (f : M₀ → M₀'), Function.Injective f → f 0 = 0 → (∀ (x y : M₀), f (x * y) = f x * f y) → ∀ [inst_4 : NoZeroDivisors M₀'], NoZeroDivisors M₀

The theorem `Function.Injective.noZeroDivisors` states that for any two types `M₀` and `M₀'` with multiplication and zero, if there exists a function `f` that is injective (meaning that equal outputs imply equal inputs), maps zero to zero and preserves multiplication (i.e., `f` of the product of two elements is equal to the product of `f` of the individual elements), then if `M₀'` has the property of having no zero divisors (no pair of nonzero elements multiply to zero), `M₀` also has this property. This theorem essentially shows that the property of having no zero divisors is preserved under injective, zero-preserving, multiplicative maps.

More concisely: If `f` is an injective function from a commutative monoid `(M₀, ∗, 0)` to another commutative monoid `(M₀', ∗', 0')` that preserves multiplication and maps zero to zero, and `M₀'` has no zero divisors, then `M₀` also has no zero divisors.