Commit 2024-09-19 13:48 8e9838b8

View on Github →

chore: Rename Holder to Hoelder in file names (#16947)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Measure/Hausdorff.lean

Renamed Mathlib/Order/JordanHolder.lean to Mathlib/Order/JordanHoelder.lean

Modified Mathlib/RingTheory/SimpleModule.lean

added def JordanHoelderModule.Iso

added theorem JordanHoelderModule.iso_symm

added theorem JordanHoelderModule.iso_trans

added theorem JordanHoelderModule.second_iso

deleted def JordanHolderModule.Iso

deleted theorem JordanHolderModule.iso_symm

deleted theorem JordanHolderModule.iso_trans

deleted theorem JordanHolderModule.second_iso

Renamed Mathlib/Topology/MetricSpace/Holder.lean to Mathlib/Topology/MetricSpace/Hoelder.lean