inv_subst

Mathlib.Tactic.CancelDenoms.Core

URI: https://scilib.ai/kg/mathlib#CancelDenoms.inv_subst

Lean4

theorem inv_subst {α} [Field α] {n k e : α} (h2 : e ≠ 0) (h3 : n * e = k) : k * (e⁻¹) = n := by
  rw [← div_eq_mul_inv, ← h3, mul_div_cancel_right₀ _ h2]

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

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

Разделы

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

Аффилиация

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