Commit 2024-07-02 08:10 d88652e5

View on Github →

chore: delay imports of Rat/Field (#14326)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/Basic.lean

deleted theorem map_ratCast_smul

deleted theorem map_rat_smul

deleted theorem ratCast_smul_eq

Modified Mathlib/Algebra/Module/Defs.lean

Modified Mathlib/Algebra/Module/Equiv.lean

Modified Mathlib/Algebra/Module/LinearMap/Basic.lean

deleted theorem AddMonoidHom.coe_toRatLinearMap

deleted def AddMonoidHom.toRatLinearMap

deleted theorem AddMonoidHom.toRatLinearMap_injective

Modified Mathlib/Algebra/Module/LinearMap/Defs.lean

Modified Mathlib/Algebra/Module/LinearMap/End.lean

Created Mathlib/Algebra/Module/LinearMap/Rat.lean

added theorem AddMonoidHom.coe_toRatLinearMap

added def AddMonoidHom.toRatLinearMap

added theorem AddMonoidHom.toRatLinearMap_injective

Created Mathlib/Algebra/Module/Rat.lean

added theorem map_ratCast_smul

added theorem map_rat_smul

added theorem ratCast_smul_eq

Modified Mathlib/Algebra/Module/Submodule/Basic.lean

Modified Mathlib/Algebra/Ring/Action/Basic.lean

deleted theorem smul_inv''

Created Mathlib/Algebra/Ring/Action/Field.lean

added theorem smul_inv''

Modified Mathlib/Algebra/Ring/Subring/Basic.lean

Modified Mathlib/Algebra/Star/Basic.lean

Modified Mathlib/Algebra/Star/Module.lean

Modified Mathlib/Analysis/NormedSpace/Basic.lean

Modified Mathlib/CategoryTheory/Linear/LinearFunctor.lean

Modified Mathlib/FieldTheory/Fixed.lean

Modified Mathlib/GroupTheory/GroupAction/ConjAct.lean

Modified Mathlib/RingTheory/Valuation/ValuationSubring.lean

Modified Mathlib/RingTheory/WittVector/Isocrystal.lean

Modified Mathlib/Topology/Instances/RealVectorSpace.lean