Commit 2023-12-08 13:37 d510164f

View on Github →

chore: tidy various files (#8880)

Estimated changes

Modified Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

Modified Mathlib/Algebra/MonoidAlgebra/Degree.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean

Modified Mathlib/CategoryTheory/Subobject/MonoOver.lean

Modified Mathlib/Combinatorics/Partition.lean

deleted theorem Nat.Partition.indiscretePartition_parts

added theorem Nat.Partition.indiscrete_parts

Modified Mathlib/Data/String/Basic.lean

Modified Mathlib/GroupTheory/Subgroup/Basic.lean

Modified Mathlib/Logic/Equiv/TransferInstance.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean

modified theorem NumberField.mixedEmbedding.adjust_f

added theorem NumberField.mixedEmbedding.convexBodyLTFactor_lt_top

added theorem NumberField.mixedEmbedding.convexBodyLTFactor_pos

added theorem NumberField.mixedEmbedding.convexBodyLT_convex

added theorem NumberField.mixedEmbedding.convexBodyLT_mem

added theorem NumberField.mixedEmbedding.convexBodyLT_symmetric

added theorem NumberField.mixedEmbedding.convexBodyLT_volume

deleted theorem NumberField.mixedEmbedding.convexBodyLtFactor_lt_top

deleted theorem NumberField.mixedEmbedding.convexBodyLtFactor_pos

deleted theorem NumberField.mixedEmbedding.convexBodyLt_convex

deleted theorem NumberField.mixedEmbedding.convexBodyLt_mem

deleted theorem NumberField.mixedEmbedding.convexBodyLt_symmetric

deleted theorem NumberField.mixedEmbedding.convexBodyLt_volume

modified theorem NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt

Modified Mathlib/NumberTheory/NumberField/Units.lean

Modified Mathlib/Topology/MetricSpace/Infsep.lean

modified theorem Set.Subsingleton.infsep_zero

modified theorem Set.einfsep_pos

modified theorem Set.einfsep_zero

modified theorem Set.le_einfsep

modified theorem Set.le_einfsep_of_forall_dist_le

Modified Mathlib/Topology/ProperMap.lean