mk'_cancel

Mathlib.GroupTheory.MonoidLocalization.Basic

URI: https://scilib.ai/kg/mathlib#Submonoid.LocalizationMap.mk'_cancel

← MathLib Explorer

English

The fraction with y in the numerator and denominator simplifies to the identity: f.mk' (y:M) y = 1.

Русский

Дробь, где числитель и знаменатель совпадают, равна единице: f.mk' (y:M) y = 1.

LaTeX

$$$ f.mk' (y: M) y = 1 $$$

Lean4

@[to_additive]
theorem mk'_cancel (a : M) (b c : S) : f.mk' (a * c) (b * c) = f.mk' a b :=
  mk'_eq_of_eq' f (by rw [Submonoid.coe_mul, mul_comm (b : M), mul_assoc])

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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