nontrivial_iff — Mathlib

English

The invariant submodule lattice ρ.invtSubmodule is nontrivial if and only if V is nontrivial.

Русский

Решетка инвариантов ρ.invtSubmodule ненуль (нетривиальна) тогда и только тогда, когда V ненулево.\n

LaTeX

$$$\\text{Nontrivial}(\\rho.invtSubmodule) \\iff \\text{Nontrivial}(V)$$$

Lean4

protected theorem nontrivial_iff : Nontrivial ρ.invtSubmodule ↔ Nontrivial V :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · contrapose! h
    infer_instance
  · refine ⟨⊥, ⊤, ?_⟩
    rw [← Subtype.coe_ne_coe, invtSubmodule.coe_top, invtSubmodule.coe_bot]
    exact bot_ne_top

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