div_self

Mathlib.Data.EReal.Inv

URI: https://scilib.ai/kg/mathlib#EReal.div_self

← MathLib Explorer

English

For a not equal to ⊥, ⊤, or 0, we have a / a = 1.

Русский

Если a не равно ⊥, ⊤ и 0, то a / a = 1.

LaTeX

$$$ a \neq \bot, a \neq \top, a \neq 0 \Rightarrow a / a = 1 $$$

Lean4

theorem div_self {a : EReal} (h₁ : a ≠ ⊥) (h₂ : a ≠ ⊤) (h₃ : a ≠ 0) : a / a = 1 :=
  by
  rw [← coe_toReal h₂ h₁] at h₃ ⊢
  rw [← coe_div, _root_.div_self (coe_ne_zero.1 h₃), coe_one]

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

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

Разделы

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

Аффилиация

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