Structures · Lean core
One
A type with a "one" element.
- Defined in
- Init.Prelude
- Shape
- One type argument · adds one
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by5
Forgetful instances
Concrete types that are instances100
- Nat
- Real
- Bool
- Quiver.Hom
- Complex
- SeparationQuotient
- NNReal
- ContinuousLinearMap
- ENNReal
- Polynomial
- Filter.Germ
- BoundedContinuousFunction
- Padic
- CStarMatrix
- RatFunc
- UniformSpace.Completion
- TensorProduct
- Unitization
- WithConv
- Matrix
- WithVal
- HahnSeries
- NonemptyInterval
- LocallyConstant
- DomMulAct
- QuadraticAlgebra
- Units
- MeasureTheory.SimpleFunc
- FreeAbelianGroup
- EReal
- MonoidAlgebra
- RestrictedProduct
- TrivSqZeroExt
- AddMonoidAlgebra
- DirectLimit
- DirectSum
- UniformFun
- DoubleCentralizer
- Zsqrtd
- UniformOnFun
- ZNum
- SymAlg
- SkewMonoidAlgebra
- Interval
- CauSeq.Completion.Cauchy
- ContMDiffMap
- OreLocalization
- PiTensorProduct
- QuaternionAlgebra
- WittVector
- SetSemiring
- PNat
- CauSeq
- TruncatedWittVector
- LucasLehmer.X
- CategoryTheory.End
- Tropical
- MvPowerSeries
- Ordinal
- FractionalIdeal
- ArithmeticFunction
- AdicCompletion
- Matrix.SpecialLinearGroup
- UpperSet
- Module.End
- LowerSet
- Cardinal
- MeasureTheory.AEEqFun
- Representation.IntertwiningMap
- Language
- AdicCompletion.AdicCauchySequence
- RingCon.Quotient
- Num
- HomogeneousLocalization
- RingQuot
- AddChar
- AlgebraicGeometry.Scheme.IdealSheafData
- Ring.DirectLimit
- CentroidHom
- Associates
- Poly
- SignType
- FreeAlgebra
- FreeGroup
- AddMonoid.End
- IncidenceAlgebra
- Equiv.Perm
- OneHom
- ContinuousMonoidHom
- ValuativeRel.ValueGroupWithZero
- MulChar
- ValuationRing.ValueGroup
- PosNum
- TangentSpace
- SubMulAction
- Part
- ModularForm
- SlashInvariantForm
- MonoidWithZeroHom
- RegularWreathProduct
How is a type an instance?
Loading the hierarchy index…
Assumed by1,470
- ComplexShape.up
- CochainComplex
- one_ne_zero
- map_one
- ComplexShape.down
- zero_lt_one
- ChainComplex
- zero_le_one
- Function.mulSupport
- Quaternion
- Set.mulIndicator
- OneHom.toFun
- Order.succ_eq_add_one
- Pi.mulSingle
- lt_add_one
- one_pos
- Function.HasFiniteMulSupport
- zero_ne_one
- SignType.cast
- castPosNum
- castNum
- Convexity.StdSimplex.weights
- Order.pred_eq_sub_one
- Set.one
- Set.NPow
- SimpleGraph.adjMatrix
- Finset.one
- HasCompactMulSupport
- castZNum
- mulTSupport
- Matrix.one_apply_ne
- Matrix.one_apply_eq
- DualNumber.eps
- Finset.npow
- mul_invOf_self
- Function.MulExact
- Set.mulIndicator_of_notMem
- enorm_one
- PEquiv.toMatrix
- Set.mulIndicator_of_mem
- Equiv.Perm.permMatrix
- one_ne_zero'
- one_le
- Pi.one_apply
- Matrix.transpose_one
- OneHom.mk.congr_simp
- invOf_mul_self
- measurable_one
- Asymptotics.isLittleO_one_iff
- SignType.coe_neg