Structures · Algebra
RingHomCompTriple
Class that expresses the fact that three ring homomorphisms form a composition triple. This is used to handle composition of semilinear maps.
- Defined in
- Mathlib.Algebra.Ring.CompTypeclasses
- Shape
- 3 explicit arguments · adds comp_eq
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by243
- LinearMap.comp
- ContinuousLinearMap.comp
- LinearEquiv.trans
- LinearMap.comp.congr_simp
- ContinuousLinearMap.comp.congr_simp
- LinearMap.comp_apply
- LinearMap.comp_assoc
- LinearMap.range_comp
- LinearIsometryEquiv.trans
- RingHomCompTriple.comp_apply
- LinearMap.compl₂
- RingHomCompTriple.comp_eq
- LinearMap.coe_comp
- ContinuousLinearEquiv.trans
- LinearMap.ker_comp
- LinearEquiv.arrowCongr
- LinearMap.compr₂ₛₗ
- LinearEquiv.trans.congr_simp
- Submodule.map_comp
- ContinuousLinearMap.comp_zero
- ContinuousLinearMap.postcomp
- ContinuousLinearMap.opNorm_comp_le
- LinearMap.llcomp
- ContinuousLinearMap.comp_assoc
- ContinuousLinearMap.precomp
- TensorProduct.map_comp
- ContinuousLinearMap.comp_apply
- ContinuousLinearMap.bilinearComp
- LinearEquiv.ker_comp
- ContinuousLinearMapWOT.comp
- LinearEquiv.arrowCongrAddEquiv
- LinearMap.range_comp_le_range
- LinearEquiv.trans_apply
- ContinuousLinearMap.zero_comp
- LinearIsometry.comp
- LinearMap.range_comp_of_range_eq_top
- LinearMap.range_le_ker_iff
- LinearMap.comp_zero
- LinearMap.ker_le_ker_comp
- TensorProduct.map_map
- ContinuousLinearMap.coe_comp
- LinearEquiv.coe_trans
- LinearMap.ker_comp_of_ker_eq_bot
- LinearEquiv.comp_toLinearMap_symm_eq
- LinearEquiv.toLinearMap_symm_comp_eq
- LinearEquiv.comp_coe
- ContinuousLinearEquiv.arrowCongrSL
- ContinuousLinearMap.compSL
- ContinuousLinearMap.add_comp
- Submodule.comap_comp
Ancestors0
No ancestors.