Structures · Algebra
RingHomInvPair
Class that expresses the fact that two ring homomorphisms are inverses of each other. This is
used to handle symm for semilinear equivalences.
- Defined in
- Mathlib.Algebra.Ring.CompTypeclasses
- Shape
- 2 explicit arguments · adds comp_eq, comp_eq₂
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- FractionRing
How is a type an instance?
Loading the hierarchy index…
Assumed by496
- LinearEquiv.toLinearMap
- ContinuousLinearEquiv.toContinuousLinearMap
- ContinuousLinearEquiv.symm
- LinearEquiv.trans
- LinearIsometryEquiv.symm
- LinearIsometryEquiv.toContinuousLinearEquiv
- ContinuousLinearEquiv.toLinearEquiv
- LinearIsometryEquiv.toLinearEquiv
- LinearEquiv.toEquiv
- LinearEquiv.ofBijective
- LinearEquiv.toAddEquiv
- TensorProduct.congr
- LinearIsometryEquiv.trans
- ContinuousLinearEquiv.toHomeomorph
- ContinuousLinearEquiv.symm_apply_apply
- LinearIsometryEquiv.toLinearIsometry
- LinearIsometryEquiv.norm_map
- LinearEquiv.conj
- ContinuousLinearEquiv.apply_symm_apply
- ContinuousLinearEquiv.trans
- LinearEquiv.invFun
- LinearEquiv.toLinearMap_injective
- LinearEquiv.arrowCongr
- LinearIsometryEquiv.apply_symm_apply
- LinearEquiv.ofInjective
- LinearEquiv.left_inv
- Finsupp.mapRange.linearEquiv
- Module.Free.of_equiv
- LinearEquiv.right_inv
- Finsupp.lcongr
- ContinuousLinearEquiv.continuous
- LinearIsometryEquiv.symm_apply_apply
- LinearEquiv.trans.congr_simp
- Submodule.equivMapOfInjective
- Submodule.orderIsoMapComap
- LinearIsometryEquiv.toHomeomorph
- LinearIsometryEquiv.toIsometryEquiv
- Finsupp.mapRange.linearEquiv_apply
- LinearEquiv.toLinearMap_inj
- LinearIsometryEquiv.continuous
- Finsupp.lcongr_single
- LinearEquiv.mk.congr_simp
- Submodule.comap_equiv_eq_map_symm
- Submodule.map_equiv_eq_comap_symm
- ContinuousLinearEquiv.injective
- Finsupp.lcongr_symm
- LinearEquiv.arrowCongrAddEquiv
- Module.Finite.of_injective
- Submodule.Quotient.equiv
- LinearEquiv.trans_apply
Ancestors0
No ancestors.