Commit 2025-02-13 17:28 dcb4fab8

View on Github →

chore(Algebra): split Zero/One instance on products (#21825) This PR is a step on the way to completely removing algebra from the dependencies of measure theory. It splits off the notation typeclass instances on Prod from the Group instances.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Prod.lean

deleted theorem Prod.fst_one

deleted theorem Prod.mk_eq_one

deleted theorem Prod.mk_one_one

deleted theorem Prod.one_eq_mk

deleted theorem Prod.snd_one

deleted theorem Prod.swap_one

Modified Mathlib/Algebra/Group/Support.lean

Created Mathlib/Algebra/ZeroOne/Prod.lean

added theorem Prod.fst_one

added theorem Prod.mk_eq_one

added theorem Prod.mk_one_one

added theorem Prod.one_eq_mk

added theorem Prod.snd_one

added theorem Prod.swap_one

Modified Mathlib/Data/Countable/Basic.lean

Modified Mathlib/Data/Finset/Image.lean

Modified Mathlib/Data/Nat/Bits.lean

Modified Mathlib/Data/Nat/Pairing.lean

Modified Mathlib/Data/Nat/Size.lean

Modified Mathlib/Logic/Encodable/Basic.lean

Modified Mathlib/Logic/Equiv/Nat.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Defs.lean