English
If f: R → S is surjective and R has an AddMonoidWithOne structure, then S inherits an AddMonoidWithOne structure via the surjection.
Русский
Если f: R → S сюръективна и R обладает структурой AddMonoidWithOne, то S наследует AddMonoidWithOne через сюръективность.
LaTeX
$$$\\exists\\; \\mathcal{S}: \\text{AddMonoidWithOne}(S)\\;\\text{from } R,$$$
Lean4
/-- A type endowed with `0`, `1` and `+` is an additive monoid with one, if it admits a surjective
map that preserves `0`, `1` and `*` from an additive monoid with one. See note
[reducible non-instances]. -/
protected abbrev addMonoidWithOne [AddMonoidWithOne R] (zero : f 0 = 0) (one : f 1 = 1)
(add : ∀ x y, f (x + y) = f x + f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (natCast : ∀ n : ℕ, f n = n) :
AddMonoidWithOne S :=
{ hf.addMonoid f zero add (swap nsmul) with
natCast := Nat.cast, natCast_zero := by rw [← natCast, Nat.cast_zero, zero]
natCast_succ := fun n => by rw [← natCast, Nat.cast_succ, add, one, natCast]
one := 1 }
