map_mem_invtSubmodule_iff — Mathlib

English

A similar equivalence to the conj_iff above without explicit conjugation notation.

Русский

Альтернатива к вышеуказанному условию равенства без явной конъюгации.

LaTeX

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

Lean4

theorem _root_.LinearEquiv.map_mem_invtSubmodule_iff {R M N : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M]
    [AddCommMonoid N] [Module R N] {f : End R N} {e : M ≃ₗ[R] N} {p : Submodule R M} :
    p.map e ∈ f.invtSubmodule ↔ p ∈ (e.symm.conj f).invtSubmodule := by simp [← e.map_mem_invtSubmodule_conj_iff]

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