coe_eq_id — Mathlib

English

Another formulation: the equivalence of f.toLinearMap with LinearMap.id is equivalent to f being the identity map.

Русский

Еще одна формулировка: эквивалентность f.toLinearMap и LinearMap.id равносильна тому, что f является тождественным отображением.

LaTeX

$$$ (f.toLinearMap = LinearMap.id) \;\iff\; f = \mathrm{id} _ _. $$$

Lean4

@[simp, norm_cast]
theorem coe_eq_id {f : M₁ →L[R₁] M₁} : (f : M₁ →ₗ[R₁] M₁) = LinearMap.id ↔ f = .id _ _ := by rw [← coe_id, coe_inj]

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