Commit 2024-04-29 09:44 d64b17d9

View on Github →

chore: split Algebra.Algebra.Basic (#12486) Splits Algebra.Algebra.Defs off Algebra.Algebra.Basic. Most imports only need the Defs file, which has significantly smaller imports. The remaining Algebra.Algebra.Basic is now a grab-bag of unrelated results, and should probably be split further or rehomed. This is mostly motivated by the wasted effort during minimization upon encountering Algebra.Algebra.Basic.

Estimated changes

deleted theorem Algebra.algebra_ext
deleted def Algebra.cast
deleted theorem Algebra.coe_linearMap
deleted theorem Algebra.commutes
deleted theorem Algebra.id.map_eq_id
deleted theorem Algebra.id.map_eq_self
deleted theorem Algebra.id.smul_eq_mul
deleted theorem Algebra.left_comm
deleted theorem Algebra.linearMap_apply
deleted def Algebra.ofModule'
deleted def Algebra.ofModule
deleted theorem Algebra.right_comm
deleted theorem Algebra.smul_def
deleted def RingHom.toAlgebra'
deleted def RingHom.toAlgebra
deleted theorem algebraMap.coe_add
deleted theorem algebraMap.coe_div
deleted theorem algebraMap.coe_inj
deleted theorem algebraMap.coe_inv
deleted theorem algebraMap.coe_mul
deleted theorem algebraMap.coe_neg
deleted theorem algebraMap.coe_one
deleted theorem algebraMap.coe_pow
deleted theorem algebraMap.coe_prod
deleted theorem algebraMap.coe_ratCast
deleted theorem algebraMap.coe_sum
deleted theorem algebraMap.coe_zero
deleted theorem algebraMap.coe_zpow
deleted def algebraMap
deleted theorem smul_algebraMap
added theorem Algebra.algebra_ext
added def Algebra.cast
added theorem Algebra.coe_linearMap
added theorem Algebra.commutes
added theorem Algebra.id.map_eq_id
added theorem Algebra.id.map_eq_self
added theorem Algebra.id.smul_eq_mul
added theorem Algebra.left_comm
added def Algebra.ofModule
added theorem Algebra.right_comm
added theorem Algebra.smul_def
added theorem algebraMap.coe_add
added theorem algebraMap.coe_div
added theorem algebraMap.coe_inj
added theorem algebraMap.coe_inv
added theorem algebraMap.coe_mul
added theorem algebraMap.coe_neg
added theorem algebraMap.coe_one
added theorem algebraMap.coe_pow
added theorem algebraMap.coe_prod
added theorem algebraMap.coe_ratCast
added theorem algebraMap.coe_sum
added theorem algebraMap.coe_zero
added theorem algebraMap.coe_zpow
added def algebraMap
added theorem smul_algebraMap