invOf_denom_swap

Mathlib.Tactic.NormNum.Eq

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.NormNum.NNRat.invOf_denom_swap

Lean4

theorem invOf_denom_swap [Semiring α] (n₁ n₂ : ℕ) (a₁ a₂ : α) [Invertible a₁] [Invertible a₂] :
    n₁ * ⅟a₁ = n₂ * ⅟a₂ ↔ n₁ * a₂ = n₂ * a₁ := by
  rw [mul_invOf_eq_iff_eq_mul_right, ← Nat.commute_cast, mul_assoc, ← mul_left_eq_iff_eq_invOf_mul, Nat.commute_cast]

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

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

Разделы

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

Аффилиация

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