English
The canonical map from FreeRing α to FreeCommRing α is surjective: every element of FreeCommRing α comes from some element of FreeRing α.
Русский
Каноническое отображение FreeRing α → FreeCommRing α сюръективно: каждый элемент FreeCommRing α является образцом некоторого элемента FreeRing α.
LaTeX
$$$\\text{Surjective}((\\uparrow) : FreeRing(\\alpha) → FreeCommRing(\\alpha))$$$
Lean4
protected theorem coe_surjective : Surjective ((↑) : FreeRing α → FreeCommRing α) := fun x => by
induction x with
| neg_one => use -1; rfl
| of b => exact ⟨FreeRing.of b, rfl⟩
| add _ _ hx hy =>
rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
exact ⟨x + y, (FreeRing.lift _).map_add _ _⟩
| mul _ _ hx hy =>
rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
exact ⟨x * y, (FreeRing.lift _).map_mul _ _⟩
