English
Pull back a NoZeroDivisors structure along an injective multiplicative map: if M0' has NoZeroDivisors and f: M0' → M0 is injective and preserves multiplication, then M0 also has NoZeroDivisors.
Русский
Перемещаем структуру NoZeroDivisors вдоль инъекции мультипликативной карты: если M0' имеет NoZeroDivisors и f: M0 → M0' инъективна и сохраняет умножение, значит и M0 имеет NoZeroDivisors.
LaTeX
$$$\\text{NoZeroDivisors } M_0'\\Rightarrow \\text{NoZeroDivisors } M_0$ (при условии инъекции и сохранения умножения)$$
Lean4
/-- Pull back a `NoZeroDivisors` instance along an injective function. -/
protected theorem noZeroDivisors [NoZeroDivisors M₀'] : NoZeroDivisors M₀ where
eq_zero_or_eq_zero_of_mul_eq_zero {a b}
H :=
have : f a * f b = 0 := by rw [← mul, H, zero]
(eq_zero_or_eq_zero_of_mul_eq_zero this).imp (fun H ↦ hf <| by rwa [zero]) fun H ↦ hf <| by rwa [zero]
