Mathlib Changelog
v4
Changelog
About
Github
Commit
2022-12-14 09:49
d1e1c996
View on Github →
feat port Algebra.Field.Basic (
#975
) fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Algebra/Field/Basic.lean
added
theorem
add_div'
added
theorem
add_div
added
theorem
add_div_eq_mul_add_div
added
theorem
div_add'
added
theorem
div_add_div
added
theorem
div_add_div_same
added
theorem
div_add_one
added
theorem
div_add_same
added
theorem
div_neg
added
theorem
div_neg_eq_neg_div
added
theorem
div_neg_self
added
theorem
div_sub'
added
theorem
div_sub_div
added
theorem
div_sub_div_same
added
theorem
div_sub_one
added
theorem
div_sub_same
added
theorem
inv_add_inv
added
theorem
inv_neg
added
theorem
inv_sub_inv'
added
theorem
inv_sub_inv
added
theorem
neg_div'
added
theorem
neg_div
added
theorem
neg_div_neg_eq
added
theorem
neg_div_self
added
theorem
neg_inv
added
theorem
of_dual_rat_cast
added
theorem
of_lex_rat_cast
added
theorem
one_add_div
added
theorem
one_div_add_one_div
added
theorem
one_div_mul_add_mul_one_div_eq_one_div_add_one_div
added
theorem
one_div_mul_sub_mul_one_div_eq_one_div_add_one_div
added
theorem
one_div_neg_eq_neg_one_div
added
theorem
one_div_neg_one_eq_neg_one
added
theorem
one_sub_div
added
theorem
same_add_div
added
theorem
same_sub_div
added
theorem
sub_div'
added
theorem
sub_div
added
theorem
to_dual_rat_cast
added
theorem
to_lex_rat_cast
Modified
Mathlib/Algebra/Ring/Basic.lean