Structures · Lean core
Inv
The notation typeclass for inverses.
This enables the notation a⁻¹ : α where a : α.
- Defined in
- Init.Prelude
- Shape
- One type argument · adds inv
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by4
Concrete types that are instances72
- Real
- Rat
- Complex
- SeparationQuotient
- NNReal
- ZMod
- ENNReal
- Filter.Germ
- RatFunc
- UniformSpace.Completion
- NNRat
- Quaternion
- WithConv
- Matrix
- WithVal
- NonemptyInterval
- LocallyConstant
- DomMulAct
- QuadraticAlgebra
- Units
- MeasureTheory.SimpleFunc
- EReal
- RestrictedProduct
- TrivSqZeroExt
- UniformFun
- UniformOnFun
- SymAlg
- Interval
- CauSeq.Completion.Cauchy
- PerfectClosure
- OreLocalization
- Tropical
- MvPowerSeries
- FractionalIdeal
- Matrix.SpecialLinearGroup
- MeasureTheory.AEEqFun
- FreeGroup
- Equiv.Perm
- OneHom
- MonCat.carrier
- ValuativeRel.ValueGroupWithZero
- MulChar
- ValuationRing.ValueGroup
- Part
- RegularWreathProduct
- GroupLike
- SpecialLinearGroup
- Con.Quotient
- Algebra.GrothendieckGroup
- AddConstEquiv
- SemidirectProduct
- Monoid.CoprodI
- CategoryTheory.PresheafOfGroups.OneCochain
- WeierstrassCurve.VariableChange
- Monoid.Coprod
- Mathlib.Tactic.FieldSimp.NF
- Subtype
- Prod
- OrderDual
- Set.Elem
- ULift
- MulOpposite
- PUnit
- Lex
- AddOpposite
- ContinuousMap
- Shrink
- Colex
- Multiplicative
- WithZero
- MonoidHom
- WithOne
How is a type an instance?
Loading the hierarchy index…
Assumed by275
- Set.inv
- Finset.inv
- MeasureTheory.mlconvolution
- Filter.Tendsto.inv₀
- MeasureTheory.Measure.inv
- ContinuousOn.inv₀
- Set.inter_inv
- List.alternatingProd
- Measurable.inv
- Measurable.fun_inv
- continuousOn_inv₀
- ContinuousOn.fun_inv₀
- Continuous.inv₀
- Continuous.fun_inv
- MulOpposite.op_inv
- Filter.Tendsto.inv
- MeasureTheory.StronglyMeasurable.inv
- Finset.zpow
- AEMeasurable.inv
- Set.mem_inv
- Set.ZPow
- Pi.inv_apply
- ContinuousAt.inv₀
- MeasureTheory.Measure.map_inv_eq_self
- AEMeasurable.fun_inv
- TrivSqZeroExt.fst_inv
- MeasureTheory.AEStronglyMeasurable.inv
- groupHomology.IsCycle₁
- groupHomology.IsCycle₂
- contMDiffAt_inv₀
- Continuous.inv
- Set.inv_preimage
- Filter.EventuallyEq.inv
- groupHomology.IsBoundary₀
- MeasurableSet.inv
- Path.inv
- groupHomology.IsBoundary₂
- groupHomology.IsBoundary₁
- ContinuousWithinAt.inv₀
- tendsto_inv₀
- TrivSqZeroExt.snd_inv
- ContinuousAt.inv
- ContinuousWithinAt.inv
- Finset.inv_nonempty_iff
- ContMDiffWithinAt.inv₀
- Set.union_inv
- Filter.inv_le_inv
- ContMDiffAt.inv₀
- Finset.Nonempty.of_inv
- ContinuousAt.fun_inv₀
Ancestors0
No ancestors.