Commit 2023-11-15 20:16 f5f44c59

View on Github →

chore: tidy various files (#8409)

Estimated changes

Modified Mathlib/Algebra/CovariantAndContravariant.lean

Modified Mathlib/Algebra/Group/UniqueProds.lean

Modified Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean

Modified Mathlib/Analysis/Convex/Cone/Proper.lean

Modified Mathlib/Data/Polynomial/Div.lean

Modified Mathlib/Data/Polynomial/Inductions.lean

Modified Mathlib/MeasureTheory/Measure/VectorMeasure.lean

Modified Mathlib/ModelTheory/Algebra/Field/Basic.lean

Modified Mathlib/Order/Filter/Basic.lean

Modified Mathlib/Order/Monotone/Basic.lean

added theorem antitoneOn_dual_iff

deleted theorem antitone_on_dual_iff

added theorem monotoneOn_dual_iff

deleted theorem monotone_on_dual_iff

added theorem strictAntiOn_dual_iff

added theorem strictAnti_dual_iff

added theorem strictMonoOn_dual_iff

added theorem strictMono_dual_iff

deleted theorem strict_anti_dual_iff

deleted theorem strict_anti_on_dual_iff

deleted theorem strict_mono_dual_iff

deleted theorem strict_mono_on_dual_iff

Modified Mathlib/Topology/AlexandrovDiscrete.lean

modified theorem subset_exterior