Commit 2023-10-03 12:58 df7b0423

View on Github →

chore: tidy various files (#7359)

Estimated changes

Modified Mathlib/Algebra/Category/GroupCat/Injective.lean

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

modified def AddMonoidAlgebra.singleZeroAlgHom

Modified Mathlib/Algebra/MonoidAlgebra/Degree.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Measurable.lean

Modified Mathlib/Analysis/InnerProductSpace/l2Space.lean

Modified Mathlib/Data/Polynomial/Derivative.lean

Modified Mathlib/Data/Real/Basic.lean

Modified Mathlib/FieldTheory/Finite/Polynomial.lean

Modified Mathlib/GroupTheory/HNNExtension.lean

Modified Mathlib/LinearAlgebra/Basis.lean

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

Modified Mathlib/ModelTheory/Fraisse.lean

deleted theorem FirstOrder.Language.Hereditary.is_equiv_invariant_of_fG

added theorem FirstOrder.Language.Hereditary.is_equiv_invariant_of_fg

Modified Mathlib/Order/Bounds/Basic.lean

Modified Mathlib/Order/OmegaCompletePartialOrder.lean

deleted theorem OmegaCompletePartialOrder.IsLUB_of_ScottContinuous

deleted theorem OmegaCompletePartialOrder.IsLUB_range_ωSup

added theorem OmegaCompletePartialOrder.isLUB_of_scottContinuous

added theorem OmegaCompletePartialOrder.isLUB_range_ωSup

deleted theorem OmegaCompletePartialOrder.ωSup_eq_of_IsLUB

added theorem OmegaCompletePartialOrder.ωSup_eq_of_isLUB

Modified Mathlib/RingTheory/Adjoin/PowerBasis.lean

Modified scripts/nolints.json