Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-06 23:05 48cc0c81

View on Github →

feat(algebra/group_with_zero): groups with a zero element adjoined (#2242)

  • feat(algebra/group_with_zero*): Basics on groups with a zero adjoined
  • feat(algebra/group_with_zero*): Basics on groups with a zero adjoined
  • Make argument implicit
  • Move inv_eq_zero out of gwz namespace
  • Partial refactor
  • Remove open_locale classical
  • Fix build
  • Factor out monoid_with_zero
  • Fix linter errors, hopefully
  • Fix build
  • Fix tests
  • Replace G with G0
  • Add spaces around ^
  • Add spaces and backticks in docstrings
  • Fix docstring of mk0
  • Fix statement of inv_eq_iff
  • Golf inv_injective
  • Golf inv_eq_zero
  • Remove the gwz namespace
  • Fix build

Estimated changes

deleted theorem div_eq_div_iff
deleted theorem div_eq_iff
deleted theorem div_eq_iff_mul_eq
deleted theorem div_eq_inv_mul
deleted theorem div_eq_mul_inv
deleted theorem div_eq_zero_iff
deleted theorem div_mul_comm
deleted theorem div_mul_div_cancel
deleted theorem div_ne_zero
deleted theorem div_ne_zero_iff
deleted theorem div_right_inj
deleted theorem divp_eq_div
deleted theorem divp_mk0
deleted theorem eq_div_iff
deleted theorem field.div_div_cancel
deleted theorem field.div_right_comm
deleted theorem inv_div
deleted theorem inv_div_left
deleted theorem inv_eq_zero
deleted theorem inv_inv''
deleted theorem inv_involutive'
deleted theorem mul_comm_div
deleted theorem mul_div_comm
deleted theorem mul_div_right_comm
deleted theorem units.inv_eq_inv
deleted def units.mk0
deleted theorem units.mk0_coe
deleted theorem units.mk0_inj
deleted theorem units.mk0_val
deleted def fpow
deleted theorem fpow_add
deleted theorem fpow_eq_gpow
deleted theorem fpow_eq_zero
deleted theorem fpow_inv
deleted theorem fpow_mul
deleted theorem fpow_ne_zero_of_ne_zero
deleted theorem fpow_neg
deleted theorem fpow_neg_mul_fpow_self
deleted theorem fpow_neg_succ_of_nat
deleted theorem fpow_of_nat
deleted theorem fpow_one
deleted theorem fpow_sub
deleted theorem fpow_zero
deleted theorem mul_fpow
deleted theorem one_fpow
deleted theorem unit_pow
deleted theorem zero_fpow
deleted theorem zero_gpow
modified def add_monoid.smul
deleted theorem div_pow
deleted theorem div_sq_cancel
deleted theorem division_ring.inv_pow
deleted theorem inv_pow'
modified def monoid.pow
deleted theorem one_div_pow
deleted theorem pow_div
deleted theorem pow_inv
added theorem coe_unit_inv_mul'
added theorem coe_unit_mul_inv'
added theorem div_div_cancel'
added theorem div_div_div_div_eq'
added theorem div_div_eq_div_mul'
added theorem div_div_eq_mul_div'
added theorem div_eq_div_iff
added theorem div_eq_iff
added theorem div_eq_iff_mul_eq
added theorem div_eq_inv_mul'
added theorem div_eq_mul_inv
added theorem div_eq_mul_one_div'
added theorem div_eq_zero_iff
added theorem div_helper'
added theorem div_mul_cancel'
added theorem div_mul_comm'
added theorem div_mul_div'
added theorem div_mul_div_cancel'
added theorem div_mul_eq_mul_div'
added theorem div_mul_left'
added theorem div_mul_right'
added theorem div_ne_zero
added theorem div_ne_zero_iff
added theorem div_one'
added theorem div_right_comm'
added theorem div_right_inj'
added theorem div_self'
added theorem div_zero'
added theorem divp_eq_div
added theorem divp_mk0
added theorem eq_div_iff
added theorem eq_mul_inv_of_mul_eq'
added theorem inv_comm_of_comm'
added theorem inv_div
added theorem inv_div_left
added theorem inv_eq_iff
added theorem inv_eq_zero
added theorem inv_inj''
added theorem inv_injective'
added theorem inv_inv''
added theorem inv_involutive'
added theorem inv_mul_cancel'
added theorem inv_ne_zero'
added theorem inv_one'
added theorem inv_zero'
added theorem mul_comm_div'
added theorem mul_div_assoc''
added theorem mul_div_cancel'''
added theorem mul_div_cancel''
added theorem mul_div_cancel_left'
added theorem mul_div_comm
added theorem mul_div_mul_left'
added theorem mul_div_mul_right'
added theorem mul_div_right_comm
added theorem mul_eq_zero'
added theorem mul_eq_zero_iff'
added theorem mul_inv''
added theorem mul_inv_cancel'
added theorem mul_inv_eq_of_eq_mul'
added theorem mul_inv_rev'
added theorem mul_left_cancel'
added theorem mul_ne_zero''
added theorem mul_ne_zero_comm''
added theorem mul_ne_zero_iff
added theorem mul_one_div_cancel'
added theorem mul_right_cancel'
added theorem mul_right_inj'
added theorem one_div
added theorem one_div_div'
added theorem one_div_mul_cancel'
added theorem one_div_mul_one_div'
added theorem one_div_ne_zero'
added theorem one_div_one'
added theorem one_div_one_div'
added theorem unit_ne_zero
added theorem units.coe_mk0
added theorem units.inv_eq_inv
added def units.mk0
added theorem units.mk0_coe
added theorem units.mk0_inj
added theorem zero_div'
added theorem div_fpow
added theorem div_pow
added theorem div_sq_cancel
added def fpow
added theorem fpow_add
added theorem fpow_add_one
added theorem fpow_coe_nat
added theorem fpow_eq_zero
added theorem fpow_inv
added theorem fpow_mul'
added theorem fpow_mul
added theorem fpow_mul_comm
added theorem fpow_ne_zero
added theorem fpow_neg
added theorem fpow_neg_mul_fpow_self
added theorem fpow_neg_one
added theorem fpow_neg_succ
added theorem fpow_neg_succ_of_nat
added theorem fpow_of_nat
added theorem fpow_one
added theorem fpow_one_add
added theorem fpow_sub
added theorem fpow_zero
added theorem inv_fpow
added theorem inv_pow'
added theorem mul_fpow
added theorem one_div_fpow
added theorem one_div_pow
added theorem one_fpow
added theorem pow_eq_zero'
added theorem pow_inv_comm'
added theorem pow_ne_zero'
added theorem pow_sub'
added theorem unit_gpow
added theorem unit_pow
added theorem zero_fpow
added theorem zero_pow'
added theorem nnreal.ne_iff