ground_id_apply

Mathlib.RingTheory.PolynomialLaw.Basic

URI: https://scilib.ai/kg/mathlib#PolynomialLaw.ground_id_apply

English

Applying ground to the identity at m yields m itself.

Русский

При применении грунтовой карты к тождественности в точке m получаем m.

LaTeX

$$$(\\mathrm{id}: M \\to_{p\\ell[R]} M).ground(m) = m$.$$

Lean4

theorem ground_id_apply (m : M) : (id : M →ₚₗ[R] M).ground m = m := by rw [ground_id, id_eq]

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

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

Разделы

Аффилиация

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