Structures · Lean core
CoeOut
CoeOut α β is for coercions that are applied from left-to-right.
- Defined in
- Init.Coe
- Shape
- 2 explicit arguments · adds coe
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Forgetful instances
Concrete types that are instances64
- Quiver.Hom
- FractionalIdeal
- AlgebraicGeometry.Scheme
- AlgEquiv
- LieSubmodule
- Ordinal.ToType
- Circle
- AlgebraicGeometry.SheafedSpace
- AlgHom
- PrincipalSeg
- LieModule.Weight
- Sym
- AlgebraicGeometry.PresheafedSpace
- GradedAlgHom
- Multiset.ToType
- LieModuleHom
- GroupLike
- AffineEquiv
- UpperHalfPlane
- RelIso
- CategoryTheory.Subobject
- DividedPowers.SubDPIdeal
- OrderRingIso
- Heyting.Regular
- GradedRingHom
- Sylow
- Lean.TSyntax
- CategoryTheory.GrothendieckTopology.Cover
- LieModuleEquiv
- ContinuousAlgEquiv
- BialgEquiv
- Matroid.Matroidᵣ
- CoalgEquiv
- CategoryTheory.MonoOver
- Qq.Quoted
- RingInvo
- StarRingEquiv
- Std.Tactic.BVDecide.LRAT.Internal.PosFin
- String.Slice.Subslice
- Lean.JsonRpc.Notification
- Lean.TSyntaxArray
- AlgebraicGeometry.Scheme.Opens
- Lean.JsonRpc.ResponseError
- Lean.JsonRpc.Response
- RayVector
- Lean.JsonRpc.Request
- DiscreteTiling.Prototile
- DividedPowers.DPMorphism
- Std.SharedMutex
- DiscreteTiling.PlacedTile
- SSet.Subcomplex
- Std.RecursiveMutex
- SubRootedTree
- Lean.Syntax.SepArray
- QuadraticMap.IsometryEquiv
- LinearMap.BilinForm.IsometryEquiv
- Lean.Syntax.TSepArray
- Mathlib.Tactic.Ring.Common.RingCompute
- Std.Mutex
- Module.Grassmannian
- AbsConvexOpenSets
- Module.End.UnifEigenvalues
- Subtype
- Fin
How is a type an instance?
Loading the hierarchy index…
Assumed by0
No theorem or definition in Mathlib takes this class as a hypothesis.
Ancestors0
No ancestors.