English
If M,N are multiplied and f: M →ₙ* N is surjective, and M is commutative, then N is commutative as well.
Русский
Если M и N коммутируют в определении умножения, и f: M →ₙ* N сюръективна, то N тоже коммутирует.
LaTeX
$$$\\text{Surjective}(f) \\Rightarrow (\\text{Std.Commutative}(\\cdot * \\cdot : N \\to N \\to N))$ given $M$ commutative and multiplicative structure.$$
Lean4
/-- If `M` and `N` have multiplications, `f : M →ₙ* N` is a surjective multiplicative map,
and `M` is commutative, then `N` is commutative. -/
@[to_additive /-- If `M` and `N` have additions, `f : M →ₙ+ N` is a surjective additive map,
and `M` is commutative, then `N` is commutative. -/
]
theorem mul_comm [Mul M] [Mul N] {f : M →ₙ* N} (is_surj : Function.Surjective f)
(is_comm : Std.Commutative (· * · : M → M → M)) : Std.Commutative (· * · : N → N → N) where
comm := fun a b ↦ by
obtain ⟨a', ha'⟩ := is_surj a
obtain ⟨b', hb'⟩ := is_surj b
simp only [← ha', ← hb', ← map_mul]
rw [is_comm.comm]
