map_symm — Mathlib

English

The symmetry of the ray map coincides with the ray map of the symmetric equivalence.

Русский

Симметрия отображения луча совпадает с отображением лучей симметрической эквивалентности.

LaTeX

$$$ (\operatorname{Module.Ray.map}(e)).\text{symm} = \operatorname{Module.Ray.map}(e^{-1}).$$$

Lean4

@[simp]
theorem map_symm (e : M ≃ₗ[R] N) : (Module.Ray.map e).symm = Module.Ray.map e.symm :=
  rfl

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