Structures · Data types

AddGroupWithOne

An AddGroupWithOne is an AddGroup with a 1. It also contains data for the unique homomorphisms ℕ → R and ℤ → R.

Defined in

Mathlib.Data.Int.Cast.Defs

Shape

One type argument · adds sub_eq_add_neg, zsmul_zero', zsmul_succ', zsmul_neg', neg_add_cancel, intCast_ofNat, intCast_negSucc