English
Surjective map f: R → S pushes forward a NonUnitalNonAssocSemiring structure from R to S.
Русский
Сюръективное отображение переносит структуру NonUnitalNonAssocSemiring из R в S.
LaTeX
$$$\\exists\\; \\mathcal{S}: \\text{NonUnitalNonAssocSemiring}(S)$$$
Lean4
/-- A type endowed with `0`, `1`, `+` is an additive commutative group with one, if it admits a
surjective map that preserves `0`, `1`, and `+` to an additive commutative group with one.
See note [reducible non-instances]. -/
protected abbrev addCommGroupWithOne [AddCommGroupWithOne R] (zero : f 0 = 0) (one : f 1 = 1)
(add : ∀ x y, f (x + y) = f x + f y) (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y)
(nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x)
(natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n) : AddCommGroupWithOne S :=
{ hf.addGroupWithOne f zero one add neg sub nsmul zsmul natCast intCast,
hf.addCommMonoid _ zero add (swap nsmul) with }
