toLinearIsometry_inj — Mathlib

English

The coercion from LinearIsometryEquiv to LinearEquiv is compatible with the toLinearEquiv projection.

Русский

Коэрция из LinearIsometryEquiv в LinearEquiv совместима с проекцией на toLinearEquiv.

LaTeX

$$$(\\mathrm{toLinearEquiv} : (E \\simeq_{\\mathrm{LI}} E') \\to (E \\simeq_{\\mathrm{L}} E'))$ is consistent with coercion$$

Lean4

@[simp]
theorem toLinearIsometry_inj {f g : E ≃ₛₗᵢ[σ₁₂] E₂} : f.toLinearIsometry = g.toLinearIsometry ↔ f = g :=
  toLinearIsometry_injective.eq_iff

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