oneLePart_leOnePart_inj — Mathlib

English

Two elements a,b are equal iff their positive and negative parts coincide: a⁺ᵐ = b⁺ᵐ and a⁻ᵐ = b⁻ᵐ.

Русский

Два элемента равны тогда и только тогда, когда их положительные и отрицательные части совпадают.

LaTeX

$$(a^{+m}=b^{+m}) ∧ (a^{-m}=b^{-m}) ⇔ a=b$$

Lean4

@[to_additive]
theorem oneLePart_leOnePart_inj : a⁺ᵐ = b⁺ᵐ ∧ a⁻ᵐ = b⁻ᵐ ↔ a = b :=
  Prod.mk_inj.symm.trans oneLePart_leOnePart_injective.eq_iff

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