cardQuot_apply

Mathlib.RingTheory.Ideal.Norm.AbsNorm

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

English

The cardQuot of a submodule S equals the cardinality of the quotient M/S.

Русский

cardQuot(S) равно кардинальности фактор-модуля M/S.

LaTeX

$$S.cardQuot = Nat.card(HasQuotient.Quotient M S)$$

Lean4

theorem cardQuot_apply (S : Submodule R M) : cardQuot S = Nat.card (M ⧸ S) := by rfl

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

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

Разделы

Аффилиация

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