cardQuot_eq_one_iff

Mathlib.RingTheory.Ideal.Norm.AbsNorm

URI: https://scilib.ai/kg/mathlib#Submodule.cardQuot_eq_one_iff

English

cardQuot P = 1 iff P = ⊤.

Русский

cardQuot(P) = 1 эквивалентно P = ⊤.

LaTeX

$$cardQuot P = 1 \iff P = ⊤$$

Lean4

@[simp]
theorem cardQuot_eq_one_iff {P : Submodule R M} : cardQuot P = 1 ↔ P = ⊤ :=
  AddSubgroup.index_eq_one.trans (by simp [SetLike.ext_iff])

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

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

Разделы

Аффилиация

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