card_relations_le_card_vars_of_isFinite

Mathlib.RingTheory.Extension.Presentation.Submersive

URI: https://scilib.ai/kg/mathlib#Algebra.PreSubmersivePresentation.card_relations_le_card_vars_of_isFinite

English

The algebra S factors through the model of HasCoeffs after base change.

Русский

Алгебра S факторизуется через модель HasCoeffs после базового изменения.

LaTeX

$$$S \\twoheadrightarrow R \\otimes_{R_0} P.ModelOfHasCoeffs R_0$$$

Lean4

theorem card_relations_le_card_vars_of_isFinite [Finite ι] : Nat.card σ ≤ Nat.card ι :=
  Nat.card_le_card_of_injective P.map P.map_inj

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

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

Разделы

Аффилиация

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