Commit 2024-04-20 13:53 4e9bd1d4

View on Github →

chore(Algebra/Algebra): split Subalgebra.Basic (#12267) This PR was supposed to be simultaneous with #12090 but I got ill last week. This is based on seeing the import Algebra.Algebra.Subalgebra.Basic → RingTheory.Ideal.Operations on the longest pole. It feels like Ideal.Operations should not be needed to define the notion of subalgebra, only to construct some interesting examples. So I removed the import and split off anything that wouldn't fit. The following results and their corollaries were split off:

  • Subalgebra.prod
  • Subalgebra.iSupLift
  • AlgHom.ker_rangeRestrict
  • Subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem

Estimated changes

deleted theorem AlgHom.ker_rangeRestrict
deleted theorem Subalgebra.coe_prod
deleted theorem Subalgebra.iSupLift_mk
deleted theorem Subalgebra.mem_prod
deleted def Subalgebra.prod
deleted theorem Subalgebra.prod_inf_prod
deleted theorem Subalgebra.prod_mono
deleted theorem Subalgebra.prod_top
added theorem Subalgebra.iSupLift_mk
added theorem Subalgebra.coe_prod
added theorem Subalgebra.mem_prod
added def Subalgebra.prod
added theorem Subalgebra.prod_mono
added theorem Subalgebra.prod_top