equivRange — Mathlib

English

The equality-based isometry on a subspace with hpq = rfl is the identity isometry on that subspace.

Русский

Изометрия, заданная равенством в случае rfl, является тождественной изометрией на подпространстве.

LaTeX

$$$ofEq p p rfl = \mathrm{LinearIsometryEquiv.refl} R' p$$$

Lean4

/-- Reinterpret a `LinearIsometry` as a `LinearIsometryEquiv` to the range. -/
@[simps! apply_coe]
noncomputable def equivRange {R S : Type*} [Semiring R] [Ring S] [Module S E] [Module R F] {σ₁₂ : R →+* S}
    {σ₂₁ : S →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : F →ₛₗᵢ[σ₁₂] E) :
    F ≃ₛₗᵢ[σ₁₂] (LinearMap.range f.toLinearMap) :=
  { f with toLinearEquiv := LinearEquiv.ofInjective f.toLinearMap f.injective }

Похожие утверждения