Commit 2024-03-07 21:56 87c01ca0

View on Github →

feat: Absolute value and positive parts in pi types (#10256) and a few more lemmas. From LeanAPAP

Estimated changes

Modified Mathlib/Algebra/GroupPower/Basic.lean

modified theorem pow_two

Modified Mathlib/Algebra/Order/Group/Abs.lean

added theorem Pi.abs_apply

added theorem Pi.abs_def

Modified Mathlib/Algebra/Order/Group/PosPart.lean

added theorem Pi.leOnePart_apply

added theorem Pi.leOnePart_def

added theorem Pi.oneLePart_apply

added theorem Pi.oneLePart_def

added theorem div_mabs_eq_inv_leOnePart_sq

added theorem leOnePart_div_oneLePart

modified theorem leOnePart_eq_inv'

modified theorem leOnePart_eq_inv

added theorem leOnePart_eq_ite

modified theorem leOnePart_eq_one'

modified theorem leOnePart_eq_one

modified theorem leOnePart_le_one'

added theorem leOnePart_mul_oneLePart

added theorem mabs_div_eq_leOnePart_sq

added theorem mabs_mul_eq_oneLePart_sq

added theorem mul_mabs_eq_oneLePart_sq

modified theorem oneLePart_div_leOnePart

added theorem oneLePart_eq_ite

modified theorem oneLePart_eq_self

modified theorem oneLePart_mul_leOnePart

added theorem one_lt_ltOnePart

added theorem one_lt_ltOnePart_iff

added theorem one_lt_oneLePart

added theorem one_lt_oneLePart_iff