Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-25 21:12 88127521

View on Github →

feat(algebra/field/basic): Semifields (#14683) Define division semirings and semifields.

Estimated changes

modified theorem add_div'
modified theorem add_div
modified theorem add_div_eq_mul_add_div
modified theorem div_add'
modified theorem div_add_div
modified theorem div_add_div_same
modified theorem div_add_one
modified theorem div_add_same
modified theorem field.to_is_field
modified theorem inv_add_inv
modified theorem is_field.nontrivial
modified structure is_field
modified theorem one_add_div
modified theorem one_div_add_one_div
modified theorem ring_hom.map_div
modified theorem ring_hom.map_eq_zero
modified theorem ring_hom.map_inv
modified theorem ring_hom.map_ne_zero
modified theorem ring_hom.map_units_inv
modified theorem same_add_div
added theorem semifield.to_is_field