Structures · Data types
AddMonoidWithOne
An AddMonoidWithOne is an AddMonoid with a 1.
It also contains data for the unique homomorphism ℕ → R.
- Defined in
- Mathlib.Data.Nat.Cast.Defs
- Shape
- One type argument · adds natCast_zero, natCast_succ
Extends3
Extended by2
Concrete types that are instances27
- Nat
- Filter.Germ
- CStarMatrix
- Matrix
- LocallyConstant
- ENat
- TrivSqZeroExt
- DirectLimit
- ZNum
- SkewMonoidAlgebra
- Tropical
- MvPowerSeries
- Ordinal
- ArithmeticFunction
- Num
- AddMonoid.End
- Subtype
- Prod
- OrderDual
- ULift
- MulOpposite
- Lex
- ContinuousMap
- Shrink
- WithTop
- WithBot
- WithZero
How is a type an instance?
Loading the hierarchy index…
Assumed by384
- Nat.cast_one
- Nat.cast_zero
- Nat.cast_add
- CharP.cast_eq_zero
- Nat.cast_nonneg'
- Nat.cast_pos'
- Nat.cast_le
- zero_lt_two
- Nat.cast_ne_zero
- Nat.cast_succ
- Nat.cast_lt
- Nat.mono_cast
- Nat.cast_inj
- two_pos
- one_lt_two
- one_add_one_eq_two
- Nat.cast_add_one
- CategoryTheory.DifferentialObject.obj
- zero_le_two
- one_le_two
- Nat.cast_injective
- nsmul_one
- Order.one_le_iff_ne_zero
- ArithmeticFunction.natToArithmeticFunction
- Nat.castEmbedding
- CategoryTheory.DifferentialObject.Hom.f
- Order.one_le_iff_pos
- CategoryTheory.DifferentialObject.d
- Nat.one_le_cast
- Nat.one_lt_cast
- OfNat.ofNat_ne_zero
- Nat.cast_eq_zero
- Nat.cast_add_one_pos
- even_two
- zero_lt_two'
- Nat.castAddMonoidHom
- Nat.cast_ite
- PosNum.cast_to_nat
- Order.lt_one_iff
- Nat.castOrderEmbedding
- Nat.strictMono_cast
- Nat.castOrderEmbedding_apply
- Nat.cast_add_one_ne_zero
- Order.le_one_iff
- zero_lt_three
- Num.cast_to_nat
- CharP.eq
- Nat.castEmbedding_apply
- zero_lt_four
- expChar_pow_pos