Structures · Lean core
NeZero
A type-class version of n ≠ 0.
- Defined in
- Init.Data.NeZero
- Shape
- One type argument · adds out
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances9
- Int
- Nat
- ENNReal
- Ordinal
- Cardinal
- MeasureTheory.Measure
- OrderType
- Fin
- Ideal
How is a type an instance?
Loading the hierarchy index…
Assumed by1,327
- one_ne_zero
- zero_lt_one
- two_ne_zero
- Nat.cast_pos'
- zero_lt_two
- lt_add_one
- Affine.Simplex.faceOpposite
- one_pos
- zero_ne_one
- add_halves
- IsPrimitiveRoot.toInteger
- two_pos
- one_lt_two
- Affine.Simplex.excenter
- NeZero.pos
- Affine.Simplex.ExcenterExists
- Affine.Simplex.touchpoint
- EuclideanHalfSpace
- Affine.Simplex.faceOppositeCentroid
- two_ne_zero'
- Affine.Simplex.excenterWeightsUnnorm
- Affine.Simplex.incenter
- modelWithCornersEuclideanHalfSpace
- RootPairing.ne_zero
- Affine.Simplex.excenterWeights
- Order.one_le_iff_ne_zero
- ZMod.toAddCircle
- Affine.Simplex.range_faceOpposite_points
- ZMod.natCast_zmod_val
- IsCyclotomicExtension.zeta_spec
- Affine.Simplex.excenterExists_empty
- Affine.Simplex.height
- Int.cast_le
- IsCyclotomicExtension.zeta
- ZMod.natCast_val
- Order.one_le_iff_pos
- ZMod.dft
- Int.cast_pos
- Affine.Simplex.altitudeFoot
- one_ne_zero'
- DirichletCharacter.LFunction
- BoxIntegral.unitPartition.box
- Affine.Simplex.exsphere
- ZMod.val_lt
- ZMod.stdAddChar
- Affine.Simplex.touchpointWeights
- Affine.Simplex.signedInfDist
- Nat.cast_add_one_pos
- Affine.Simplex.exradius
- add_self_div_two
Ancestors0
No ancestors.