Structures · Lean core
Mul
The homogeneous version of HMul: a * b : α where a b : α.
- Defined in
- Init.Prelude
- Shape
- One type argument · adds mul
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by6
Forgetful instances
Concrete types that are instances100
- Int
- Nat
- Real
- Rat
- Bool
- Quiver.Hom
- Complex
- SeparationQuotient
- BitVec
- ContinuousLinearMap
- Polynomial
- Filter.Germ
- BoundedContinuousFunction
- Padic
- CStarMatrix
- RatFunc
- UniformSpace.Completion
- UInt64
- TensorProduct
- UInt8
- UInt16
- UInt32
- Unitization
- WithConv
- Matrix
- WithVal
- HahnSeries
- NonemptyInterval
- LocallyConstant
- USize
- DomMulAct
- QuadraticAlgebra
- Units
- MeasureTheory.SimpleFunc
- FreeAbelianGroup
- EReal
- MonoidAlgebra
- RestrictedProduct
- TrivSqZeroExt
- AddMonoidAlgebra
- DirectLimit
- Finsupp
- DirectSum
- UniformFun
- DoubleCentralizer
- Zsqrtd
- UniformOnFun
- ZNum
- SymAlg
- SkewMonoidAlgebra
- Interval
- ContinuousMapZero
- CauSeq.Completion.Cauchy
- PerfectClosure
- ContMDiffMap
- OreLocalization
- PiTensorProduct
- QuaternionAlgebra
- ZeroAtInftyContinuousMap
- Int32
- Int8
- Int64
- Int16
- WittVector
- PNat
- CauSeq
- TruncatedWittVector
- LucasLehmer.X
- CategoryTheory.End
- Tropical
- MvPowerSeries
- FractionalIdeal
- ArithmeticFunction
- AdicCompletion
- Matrix.SpecialLinearGroup
- UpperSet
- Module.End
- LowerSet
- Cardinal
- MeasureTheory.AEEqFun
- ISize
- Representation.IntertwiningMap
- Language
- AdicCompletion.AdicCauchySequence
- RingCon.Quotient
- Num
- HomogeneousLocalization
- RingQuot
- AlgebraicGeometry.Scheme.IdealSheafData
- CentroidHom
- Associates
- Poly
- SignType
- FreeAlgebra
- FreeGroup
- CompactlySupportedContinuousMap
- AddMonoid.End
- IncidenceAlgebra
- Equiv.Perm
- GradedTensorProduct
How is a type an instance?
Loading the hierarchy index…
Assumed by2,904
- map_mul
- neg_mul
- Commute
- mul_neg
- RingEquiv.symm
- MulEquiv.symm
- mul_add
- MulLeftMono
- add_mul
- mul_le_mul_of_nonneg_left
- smul_eq_mul
- mul_le_mul_of_nonneg_right
- Set.mul
- mul_le_mul'
- MulRightMono
- IsIdempotentElem
- dotProduct
- mul_ne_zero
- norm_mul
- Subsemigroup.carrier
- mul_ite
- MulAut
- Finset.mul
- MulLeftStrictMono
- mul_le_mul
- IsSquare
- MulEquiv.toEquiv
- RingCon.Quotient
- MulRightStrictMono
- RingEquiv.toEquiv
- SemiconjBy
- IsLeftRegular
- IsRightRegular
- Commute.eq
- ite_mul
- Commute.symm
- smul_mul_assoc
- Filter.Tendsto.mul
- RingEquiv.refl
- mul_lt_mul_of_pos_left
- RingCon.toQuotient
- mul_smul_comm
- MulEquivClass.toMulEquiv
- Set.centralizer
- mul_right_inj'
- Filter.Tendsto.const_mul
- Matrix.hadamard
- mul_lt_mul_of_pos_right
- RingEquiv.trans
- MulEquiv.trans