le_normalizer

Mathlib.Algebra.Lie.Normalizer

URI: https://scilib.ai/kg/mathlib#LieSubmodule.le_normalizer

English

The normalizer distributes over intersections: (N1 ∩ N2).normalizer = N1.normalizer ∩ N2.normalizer.

Русский

Нормализатор сохраняет пересечения: (N1 ∩ N2).normalizer = N1.normalizer ∩ N2.normalizer.

LaTeX

$$$ (N_1 \\cap N_2).normalizer = N_1.normalizer \\cap N_2.normalizer $$$

Lean4

@[simp]
theorem le_normalizer : N ≤ N.normalizer := by
  intro m hm
  rw [mem_normalizer]
  exact fun x => N.lie_mem hm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru