iterateMapComap — Mathlib

English

For a linear equivalence e, p.map e ∈ (e.conj f).invtSubmodule iff p ∈ f.invtSubmodule.

Русский

Пусть e — линейное соответствие; p.map e ∈ (e.conj f).invtSubmodule тогда и только тогда, когда p ∈ f.invtSubmodule.

LaTeX

$$$p.map e \in (e.conj f).invtSubmodule \iff p \in f.invtSubmodule$$$

Lean4

/-- The `LinearMap.iterateMapComap f i n K : Submodule R N` is
`f⁻¹(i(⋯(f⁻¹(i(K)))))` (`n` times). -/
def iterateMapComap (n : ℕ) :=
  (fun K : Submodule R N ↦ (K.map i).comap f)^[n]

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