Theorems · Definition · functional analysis
ContinuousLinearEquiv.trans
{R₁ : Type u_1} →
{R₂ : Type u_2} →
{R₃ : Type u_3} →
[inst : Semiring R₁] →
[inst_1 : Semiring R₂] →
[inst_2 : Semiring R₃] →
{σ₁₂ : R₁ →+* R₂} →
{σ₂₁ : R₂ →+* R₁} →
[inst_3 : RingHomInvPair σ₁₂ σ₂₁] →
[inst_4 : RingHomInvPair σ₂₁ σ₁₂] →
{σ₂₃ : R₂ →+* R₃} →
{σ₃₂ : R₃ →+* R₂} →
[inst_5 : RingHomInvPair σ₂₃ σ₃₂] →
[inst_6 : RingHomInvPair σ₃₂ σ₂₃] →
{σ₁₃ : R₁ →+* R₃} →
{σ₃₁ : R₃ →+* R₁} →
[inst_7 : RingHomInvPair σ₁₃ σ₃₁] →
[inst_8 : RingHomInvPair σ₃₁ σ₁₃] →
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] →
[RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] →
{M₁ : Type u_4} →
[inst_11 : TopologicalSpace M₁] →
[inst_12 : AddCommMonoid M₁] →
{M₂ : Type u_5} →
[inst_13 : TopologicalSpace M₂] →
[inst_14 : AddCommMonoid M₂] →
{M₃ : Type u_6} →
[inst_15 : TopologicalSpace M₃] →
[inst_16 : AddCommMonoid M₃] →
[inst_17 : Module R₁ M₁] →
[inst_18 : Module R₂ M₂] →
[inst_19 : Module R₃ M₃] →
(M₁ ≃SL[σ₁₂] M₂) → (M₂ ≃SL[σ₂₃] M₃) → M₁ ≃SL[σ₁₃] M₃The composition of two continuous linear equivalences as a continuous linear equivalence.
- Defined in
- Mathlib.Topology.Algebra.Module.Equiv
- Cited by
- 31 results in Mathlib
- Foundations
- Depth 29 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- Modulestatement and proof · cited by 20,661
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- RingHomstatement and proof · cited by 10,189
- LinearEquivproof · cited by 3,317
- ContinuousLinearEquivstatement and proof · cited by 743
- RingHomInvPairstatement and proof · cited by 523
- LinearEquiv.transproof · cited by 298
- RingHomCompTriplestatement and proof · cited by 234
- ContinuousLinearEquiv.toLinearEquivproof · cited by 118
Cited by40
Results whose statement or proof uses this declaration.
- starL'proof · cited by 15
- ContRepresentation.Equiv.transproof · cited by 5
- PiLp.equivOfUniqueproof · cited by 3
- ContinuousLinearMap.inverse_comp_equivproof · cited by 3
- ContinuousLinearMap.inverse_equiv_compproof · cited by 3
- isImmersionOfComplement_subtypeVal_Iccproof · cited by 3
- Manifold.IsSubmersionAtOfComplement.trans_Fproof · cited by 2
- ContinuousLinearMap.inverse_eq_ringInverseproof · cited by 2
- integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrableproof · cited by 2
- ZLattice.volume_image_eq_volume_div_covolume'proof · cited by 2
- Manifold.IsImmersionAtOfComplement.prodMapproof · cited by 2
- Manifold.IsImmersionAtOfComplement.trans_Fproof · cited by 2