absNorm_apply

Mathlib.RingTheory.Ideal.Norm.AbsNorm

URI: https://scilib.ai/kg/mathlib#Ideal.absNorm_apply

English

This is the identity absNorm I = cardQuot I for the given structure of S and I.

Русский

Эта лемма повторяет идентичность absNorm I = cardQuot I при заданной структуре S и I.

LaTeX

$$$\\forall I:\\; \\text{absNorm}(I) = \\text{cardQuot}(I)$$$

Lean4

theorem absNorm_apply (I : Ideal S) : absNorm I = cardQuot I :=
  rfl

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

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

Разделы

Аффилиация

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