Structures · Lean core
Div
The homogeneous version of HDiv: a / b : α where a b : α.
- Defined in
- Init.Prelude
- Shape
- One type argument · adds div
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by3
Forgetful instances
Concrete types that are instances68
- Int
- Nat
- Rat
- SeparationQuotient
- NNReal
- BitVec
- Polynomial
- Filter.Germ
- Padic
- RatFunc
- UInt64
- NNRat
- UInt8
- UInt16
- UInt32
- WithVal
- NonemptyInterval
- LocallyConstant
- USize
- QuadraticAlgebra
- Units
- MeasureTheory.SimpleFunc
- RestrictedProduct
- UniformFun
- UniformOnFun
- ZNum
- Interval
- Int32
- Int8
- Int64
- Int16
- GaussianInt
- Tropical
- Ordinal
- FractionalIdeal
- UpperSet
- LowerSet
- MeasureTheory.AEEqFun
- ISize
- Num
- OneHom
- Part
- SpecialLinearGroup
- Con.Quotient
- AddConstEquiv
- Float
- Float32
- Std.Time.Month.Offset
- Float32.Model
- Float.Model
- System.FilePath
- Float.Model.UnpackedFloat.Sign
- Subtype
- Prod
- OrderDual
- Set.Elem
- ULift
- Fin
- PUnit
- Lex
- AddOpposite
- ContinuousMap
- Shrink
- Colex
- Multiplicative
- Submodule
- WithZero
- MonoidHom
How is a type an instance?
Loading the hierarchy index…
Assumed by276
- Set.div
- mul_div_cancel_left₀
- mul_div_cancel_right₀
- Finset.div
- LinearGrowth.linearGrowthInf
- LinearGrowth.linearGrowthSup
- Pi.div_apply
- AEMeasurable.div_const
- Measurable.div
- Filter.Tendsto.div'
- Filter.EventuallyEq.div
- MonoidHom.commutatorMap
- LinearGrowth.linearGrowthInf_le_linearGrowthSup
- Measurable.fun_div
- MeasureTheory.StronglyMeasurable.div'
- Finset.mem_div
- Continuous.fun_div'
- ite_div
- ProbabilityTheory.Kernel.iIndepFun.indepFun_div_left
- Set.div_subset_div_left
- ProbabilityTheory.Kernel.iIndepFun.indepFun_div_div
- Finset.div_empty
- Finset.empty_div
- Filter.le_div_iff
- AEMeasurable.div
- Filter.Tendsto.div_const'
- ProbabilityTheory.Kernel.iIndepFun.indepFun_div_right
- ContinuousWithinAt.div'
- ProbabilityTheory.Kernel.iIndepFun.indepFun_div_left₀
- ContinuousAt.fun_div'
- Finset.coe_div
- Set.MapsTo.div
- Set.div_mem_div
- Filter.div_mem_div
- Measurable.const_div
- Set.singleton_div_singleton
- Finset.card_div_le
- div_dite
- Finset.div_mem_div
- AEMeasurable.fun_div
- Set.iUnion_div_left_image
- Set.div_subset_div_right
- Part.right_dom_of_div_dom
- ProbabilityTheory.Kernel.iIndepFun.indepFun_div_div₀
- ProbabilityTheory.Kernel.iIndepFun.indepFun_div_right₀
- ContinuousOn.div'
- Set.mem_div
- dite_div
- dite_div_dite
- Continuous.div'