Commit 2023-12-04 08:33 8c4338d2

View on Github →

chore: tidy various files (#8560)

Estimated changes

Modified Mathlib/Algebra/Associated.lean

Modified Mathlib/Algebra/Group/TypeTags.lean

Modified Mathlib/Algebra/Order/WithZero.lean

Modified Mathlib/Analysis/Analytic/Constructions.lean

Modified Mathlib/Analysis/Convex/Topology.lean

added theorem JoinedIn.of_segment_subset

deleted theorem JoinedIn_of_segment_subset

Modified Mathlib/Analysis/NormedSpace/Connected.lean

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

modified theorem ContinuousMultilinearMap.continuous_eval

Modified Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean

Modified Mathlib/Analysis/NormedSpace/Star/Unitization.lean

Modified Mathlib/Geometry/Euclidean/Inversion/Calculus.lean

Modified Mathlib/GroupTheory/GroupAction/Basic.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

Modified Mathlib/RingTheory/Nilpotent.lean

Modified Mathlib/RingTheory/Polynomial/Nilpotent.lean

Modified Mathlib/Tactic/Nontriviality/Core.lean

Modified Mathlib/Topology/UnitInterval.lean