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