map_refl — Mathlib

English

The map corresponding to the identity linear equivalence acts as the identity on rays.

Русский

Отображение, соответствующее тождественной линейной эквивалентности, действует как тождественное на лучах.

LaTeX

$$$ \operatorname{Module.Ray.map}(\operatorname{LinearEquiv.refl}(R,M)) = \operatorname{Equiv.refl}(\operatorname{Module.Ray}(R,M)). $$$

Lean4

@[simp]
theorem map_refl : (Module.Ray.map <| LinearEquiv.refl R M) = Equiv.refl _ :=
  Equiv.ext <| Module.Ray.ind R fun _ _ => rfl

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