eq_zero_of_num_eq_zero

Mathlib.RingTheory.Localization.NumDen

URI: https://scilib.ai/kg/mathlib#IsFractionRing.eq_zero_of_num_eq_zero

← MathLib Explorer

English

The same associativity result as in 180488 holds in the inverse context.

Русский

Та же ассоциативность деноминатора и числителя в обратном контексте.

LaTeX

$$$\\operatorname{Associated}(\\mathrm{den}_A(x), \\mathrm{num}_A(x^{-1}))$$$

Lean4

theorem eq_zero_of_num_eq_zero {x : K} (h : num A x = 0) : x = 0 :=
  (num_mul_den_eq_num_iff_eq' (A := A)).mp (by rw [zero_mul, h, RingHom.map_zero])

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

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

Разделы

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

Аффилиация

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