Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-24 04:03 b7af2838

View on Github →

feat(algebra): define invertible typeclass (#2504) In the discussion for #2480, we decided that the definitions would be cleaner if the elaborator could supply us with a suitable value of 1/2. With these changes, we can now add an [invertible 2] argument to write ⅟ 2. Related to Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.232480.20bilinear.20forms

Estimated changes

Modified src/algebra/group/basic.lean

added theorem left_inv_eq_right_inv

Created src/algebra/invertible.lean

added theorem div_mul_cancel_of_invertible

added theorem div_self_of_invertible

added theorem inv_mul_cancel_of_invertible

added theorem inv_of_div

added theorem inv_of_eq_group_inv

added theorem inv_of_eq_inv

added theorem inv_of_eq_right_inv

added theorem inv_of_inv_of

added theorem inv_of_mul

added theorem inv_of_mul_self

added theorem inv_of_neg

added theorem inv_of_one

added def invertible_div

added def invertible_inv

added def invertible_inv_of

added def invertible_mul

added def invertible_neg

added def invertible_of_group

added def invertible_of_nonzero

added def invertible_one

added theorem is_unit_of_invertible

added theorem mul_div_cancel_of_invertible

added theorem mul_inv_cancel_of_invertible

added theorem mul_inv_of_mul_self_cancel

added theorem mul_inv_of_self

added theorem mul_mul_inv_of_self_cancel

added theorem nonzero_of_invertible