Commit 2025-06-10 22:59 0ca225f9

View on Github →

chore: split Mathlib/Topology/Algebra/RestrictedProduct (#25558) Mathlib/Topology/Algebra/RestrictedProduct.lean is over 1000 lines and we have over 500 lines more of restricted product API in FLT with more to come, so I thought I would split sooner rather than later.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean

Created Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean

added theorem RestrictedProduct.div_apply

added def RestrictedProduct.evalMonoidHom

added theorem RestrictedProduct.evalMonoidHom_apply

added def RestrictedProduct.evalRingHom

added theorem RestrictedProduct.evalRingHom_apply

added theorem RestrictedProduct.eventually

added theorem RestrictedProduct.exists_inclusion_eq_of_eventually

added theorem RestrictedProduct.exists_structureMap_eq_of_forall

added theorem RestrictedProduct.ext

added def RestrictedProduct.inclusion

added theorem RestrictedProduct.inclusion_eq_id

added theorem RestrictedProduct.inv_apply

added def RestrictedProduct.map

added def RestrictedProduct.mapMonoidHom

added theorem RestrictedProduct.mapMonoidHom_apply

added def RestrictedProduct.mapRingHom

added theorem RestrictedProduct.mapRingHom_apply

added theorem RestrictedProduct.map_apply

added theorem RestrictedProduct.mul_apply

added theorem RestrictedProduct.one_apply

added theorem RestrictedProduct.pow_apply

added theorem RestrictedProduct.range_coe

added theorem RestrictedProduct.range_coe_principal

added theorem RestrictedProduct.range_inclusion

added theorem RestrictedProduct.range_structureMap

added theorem RestrictedProduct.smul_apply

added def RestrictedProduct.structureMap

added theorem RestrictedProduct.zpow_apply

added def RestrictedProduct

Renamed Mathlib/Topology/Algebra/RestrictedProduct.lean to Mathlib/Topology/Algebra/RestrictedProduct/TopologicalSpace.lean

deleted theorem RestrictedProduct.div_apply

deleted def RestrictedProduct.evalMonoidHom

deleted theorem RestrictedProduct.evalMonoidHom_apply

deleted def RestrictedProduct.evalRingHom

deleted theorem RestrictedProduct.evalRingHom_apply

deleted theorem RestrictedProduct.eventually

deleted theorem RestrictedProduct.exists_inclusion_eq_of_eventually

deleted theorem RestrictedProduct.exists_structureMap_eq_of_forall

deleted theorem RestrictedProduct.ext

deleted def RestrictedProduct.inclusion

deleted theorem RestrictedProduct.inclusion_eq_id

deleted theorem RestrictedProduct.inv_apply

deleted def RestrictedProduct.map

deleted def RestrictedProduct.mapMonoidHom

deleted theorem RestrictedProduct.mapMonoidHom_apply

deleted def RestrictedProduct.mapRingHom

deleted theorem RestrictedProduct.mapRingHom_apply

deleted theorem RestrictedProduct.map_apply

deleted theorem RestrictedProduct.mul_apply

deleted theorem RestrictedProduct.one_apply

deleted theorem RestrictedProduct.pow_apply

deleted theorem RestrictedProduct.range_coe

deleted theorem RestrictedProduct.range_coe_principal

deleted theorem RestrictedProduct.range_inclusion

deleted theorem RestrictedProduct.range_structureMap

deleted theorem RestrictedProduct.smul_apply

deleted def RestrictedProduct.structureMap

deleted theorem RestrictedProduct.zpow_apply

deleted def RestrictedProduct

Modified scripts/noshake.json