Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-07-09 11:47
a1a59671
View on Github →
chore: postpone Field past Algebra/Defs (
#14465
)
Estimated changes
Modified
Mathlib.lean
Modified
Mathlib/Algebra/Algebra/Defs.lean
deleted
theorem
algebraMap.coe_div
deleted
theorem
algebraMap.coe_inj
deleted
theorem
algebraMap.coe_inv
deleted
theorem
algebraMap.coe_ratCast
deleted
theorem
algebraMap.coe_zpow
deleted
theorem
algebraMap.lift_map_eq_zero_iff
Created
Mathlib/Algebra/Algebra/Field.lean
added
theorem
algebraMap.coe_div
added
theorem
algebraMap.coe_inj
added
theorem
algebraMap.coe_inv
added
theorem
algebraMap.coe_ratCast
added
theorem
algebraMap.coe_zpow
added
theorem
algebraMap.lift_map_eq_zero_iff
Modified
Mathlib/Algebra/Field/Subfield.lean
Modified
Mathlib/Algebra/Ring/CentroidHom.lean
Modified
Mathlib/Analysis/RCLike/Basic.lean