eq_eq_cancel_eq

Mathlib.Tactic.FieldSimp.Lemmas

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq

Lean4

theorem eq_eq_cancel_eq {M : Type*} [CancelMonoidWithZero M] {e₁ e₂ f₁ f₂ L : M} (H₁ : e₁ = L * f₁) (H₂ : e₂ = L * f₂)
    (HL : L ≠ 0) : (e₁ = e₂) = (f₁ = f₂) := by
  subst H₁ H₂
  rw [mul_right_inj' HL]

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

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

Разделы

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

Аффилиация

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