cardQuot — Mathlib

English

The quotient's cardinal equals the index of the additive subgroup: cardQuot S = index of S in M’s additive group.

Русский

Так какcardQuot(S) равен индексу подгруппы S в аддитивную группу M.

LaTeX

$$S.cardQuot = |M / S| = [M : S]$$

Lean4

/-- The cardinality of `(M ⧸ S)`, if `(M ⧸ S)` is finite, and `0` otherwise.
This is used to define the absolute ideal norm `Ideal.absNorm`.
-/
noncomputable def cardQuot (S : Submodule R M) : ℕ :=
  AddSubgroup.index S.toAddSubgroup

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