Commit 2023-07-31 15:32 ff15b399

View on Github →

chore: tidy various files (#6174)

Estimated changes

Modified Mathlib/Data/Finset/Powerset.lean

added def Finset.decidableExistsOfDecidableSSubsets'

deleted def Finset.decidableExistsOfDecidableSsubsets'

added def Finset.decidableForallOfDecidableSSubsets'

deleted def Finset.decidableForallOfDecidableSsubsets'

added theorem Finset.powersetLen_sup

deleted theorem Finset.powerset_len_sup

Modified Mathlib/Data/Set/Lattice.lean

Modified Mathlib/Data/Sign.lean

deleted inductive SignType.Le

modified def SignType.castHom

modified def SignType.fin3Equiv

modified theorem SignType.univ_eq

Modified Mathlib/Deprecated/Subgroup.lean

Modified Mathlib/GroupTheory/Coset.lean

added def Subgroup.quotientEquivProdOfLE'

deleted def Subgroup.quotientEquivProdOfLe'

added def Subgroup.quotientMapOfLE

added theorem Subgroup.quotientMapOfLE_apply_mk

deleted def Subgroup.quotientMapOfLe

deleted theorem Subgroup.quotientMapOfLe_apply_mk

added def Subgroup.quotientSubgroupOfEmbeddingOfLE

added theorem Subgroup.quotientSubgroupOfEmbeddingOfLE_apply_mk

deleted def Subgroup.quotientSubgroupOfEmbeddingOfLe

deleted theorem Subgroup.quotientSubgroupOfEmbeddingOfLe_apply_mk

added def Subgroup.quotientSubgroupOfMapOfLE

added theorem Subgroup.quotientSubgroupOfMapOfLE_apply_mk

deleted def Subgroup.quotientSubgroupOfMapOfLe

deleted theorem Subgroup.quotientSubgroupOfMapOfLe_apply_mk

Modified Mathlib/GroupTheory/Index.lean

Modified Mathlib/Order/Filter/Germ.lean

Modified Mathlib/Order/Grade.lean

Modified Mathlib/Order/OmegaCompletePartialOrder.lean

modified def OmegaCompletePartialOrder.ContinuousHom.flip

Modified Mathlib/RingTheory/MvPolynomial/Symmetric.lean

Modified Mathlib/Tactic/IntervalCases.lean

Modified Mathlib/Topology/Algebra/Monoid.lean

modified def Submonoid.topologicalClosure

Modified Mathlib/Topology/Order.lean