Commit 2023-02-02 10:19 ec8fde78

View on Github →

chore: tidy various files (#2009)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Fin.lean

added theorem Fin.prod_Ioi_succ

added theorem Fin.prod_Ioi_zero

deleted theorem Fin.prod_ioi_succ

deleted theorem Fin.prod_ioi_zero

Modified Mathlib/Algebra/BigOperators/Intervals.lean

added theorem Finset.prod_Ico_eq_prod_range

deleted theorem Finset.prod_ico_eq_prod_range

Modified Mathlib/Algebra/Order/Ring/WithTop.lean

Modified Mathlib/Combinatorics/SetFamily/Intersecting.lean

added theorem Set.Intersecting.isUpperSet'

deleted theorem Set.Intersecting.is_upper_set'

Modified Mathlib/Data/Finset/Option.lean

deleted theorem Finset.eraseNone_eq_bUnion

added theorem Finset.eraseNone_eq_bunionᵢ

added theorem Finset.eraseNone_insertNone

deleted theorem Finset.eraseNone_insert_none

added theorem Finset.insertNone_eraseNone

deleted theorem Finset.insert_none_eraseNone

Modified Mathlib/Data/Set/Semiring.lean

Modified Mathlib/GroupTheory/Subgroup/Pointwise.lean

Modified Mathlib/GroupTheory/Submonoid/Pointwise.lean

added theorem AddSubmonoid.natCast_mem_one

deleted theorem AddSubmonoid.nat_cast_mem_one

deleted theorem AddSubmonoid.pointwise_central_scalar

added theorem AddSubmonoid.pointwise_isCentralScalar

deleted theorem Submonoid.pointwise_central_scalar

added theorem Submonoid.pointwise_isCentralScalar

Modified Mathlib/Order/CompleteLattice.lean

deleted theorem Sup_prod

deleted theorem infₛ_Prod

added theorem infₛ_prod

added theorem supₛ_prod

Modified Mathlib/Order/Ideal.lean

added theorem Order.Ideal.IsMaximal.isCoatom'

deleted theorem Order.Ideal.IsMaximal.is_coatom'

modified def Order.idealOfCofinals