Mathlib Changelog
v3
Changelog
About
Github
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
src/algebra/field/basic.lean
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
not_is_field_of_subsingleton
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
Modified
src/data/complex/basic.lean
Modified
src/data/real/nnreal.lean
Modified
src/number_theory/cyclotomic/basic.lean
Modified
src/ring_theory/ideal/quotient.lean
modified
theorem
ideal.quotient.maximal_ideal_iff_is_field_quotient
Modified
src/ring_theory/witt_vector/basic.lean