coe_ofInvolutive — Mathlib

English

If f is involutive (f^2 = id) and f is a linear map, then the associated linear equivalence built from f has the same underlying function f.

Русский

Если f инволютивно (f^2 = id) и линейное отображение, то соответствующее линейное эквивалентное отображение имеет ту же функцию f.

LaTeX

$$coe_ofInvolutive : (ofInvolutive f hf) = f$$

Lean4

@[simp]
theorem coe_ofInvolutive {σ σ' : R →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {_ : Module R M} (f : M →ₛₗ[σ] M)
    (hf : Involutive f) : ⇑(ofInvolutive f hf) = f :=
  rfl

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