Commit 2023-06-26 01:04 f6a68c55

View on Github →

chore: tidy various files (#5469)

Estimated changes

Modified Archive/Wiedijk100Theorems/AbelRuffini.lean

modified theorem AbelRuffini.coeff_zero_Phi

modified theorem AbelRuffini.degree_Phi

Modified Mathlib/Algebra/Homology/LocalCohomology.lean

deleted theorem Ideal.exists_pow_le_of_le_radical_of_fG

added theorem Ideal.exists_pow_le_of_le_radical_of_fg

added def localCohomology.SelfLERadical

deleted def localCohomology.SelfLeRadical

added def localCohomology.idealPowersToSelfLERadical

added def localCohomology.idealPowersToSelfLERadicalCompInclusion

deleted def localCohomology.idealPowersToSelfLeRadical

deleted def localCohomology.idealPowersToSelfLeRadicalCompInclusion

added def localCohomology.ofSelfLERadical

deleted def localCohomology.ofSelfLeRadical

added def localCohomology.selfLERadicalDiagram

deleted def localCohomology.selfLeRadicalDiagram

Modified Mathlib/Data/Set/Ncard.lean

deleted theorem Set.Finite_of_ncard_ne_zero

deleted theorem Set.Finite_of_ncard_pos

deleted theorem Set.exists_intermediate_Set'

added theorem Set.exists_intermediate_set'

deleted theorem Set.exists_smaller_Set

added theorem Set.exists_smaller_set

added theorem Set.finite_of_ncard_ne_zero

added theorem Set.finite_of_ncard_pos

deleted theorem Set.ncard_eq_ofBijective

added theorem Set.ncard_eq_of_bijective

deleted theorem Set.ncard_image_ofInjective

added theorem Set.ncard_image_of_injective

deleted theorem Set.ncard_preimage_ofInjective_subset_range

added theorem Set.ncard_preimage_of_injective_subset_range

Modified Mathlib/Geometry/Euclidean/Circumcenter.lean

Modified Mathlib/Geometry/Manifold/Algebra/Monoid.lean

Modified Mathlib/MeasureTheory/Covering/LiminfLimsup.lean

Modified Mathlib/NumberTheory/ClassNumber/Finite.lean

Modified Mathlib/RingTheory/ClassGroup.lean