ucs_eq_self_of_normalizer_eq_self

English

If a submodule N1 is equal to its normalizer, then its UCS equals N1 for every k.

Русский

Если N1 равно своему нормализатору, то N1.ucs k = N1 для всякого k.

LaTeX

$$$\\operatorname{N}_1.normalizer = N_1 \\Rightarrow \\forall k, N_1.ucs k = N_1.$$$

Lean4

theorem ucs_eq_self_of_normalizer_eq_self (h : N₁.normalizer = N₁) (k : ℕ) : N₁.ucs k = N₁ := by
  induction k with
  | zero => simp
  | succ k ih => rwa [ucs_succ, ih]

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