Commit 2024-04-08 08:20 1f25ef62

View on Github →

chore: rename IsRoot.definition back to IsRoot.def (#11999)

Estimated changes

Modified Archive/Imo/Imo2006Q5.lean

Modified Mathlib/Algebra/LinearRecurrence.lean

Modified Mathlib/Algebra/Polynomial/Degree/Definitions.lean

deleted theorem Polynomial.Monic.def'

added theorem Polynomial.Monic.def

Modified Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean

added theorem Polynomial.TrailingMonic.def

deleted theorem Polynomial.TrailingMonic.definition

Modified Mathlib/Algebra/Polynomial/Div.lean

Modified Mathlib/Algebra/Polynomial/Eval.lean

added theorem Polynomial.IsRoot.def

deleted theorem Polynomial.IsRoot.definition

Modified Mathlib/Algebra/Polynomial/FieldDivision.lean

Modified Mathlib/Algebra/Polynomial/Monic.lean

Modified Mathlib/Algebra/Polynomial/RingDivision.lean

Modified Mathlib/Algebra/Polynomial/Splits.lean

deleted theorem Polynomial.Splits.def'

added theorem Polynomial.Splits.def

Modified Mathlib/Analysis/Asymptotics/Asymptotics.lean

added theorem Asymptotics.IsLittleO.def

deleted theorem Asymptotics.IsLittleO.definition

Modified Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean

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

Modified Mathlib/Analysis/Calculus/Rademacher.lean

Modified Mathlib/Analysis/SpecificLimits/Normed.lean

Modified Mathlib/CategoryTheory/Generator.lean

deleted theorem CategoryTheory.IsCodetector.def'

added theorem CategoryTheory.IsCodetector.def

deleted theorem CategoryTheory.IsCoseparator.def'

added theorem CategoryTheory.IsCoseparator.def

deleted theorem CategoryTheory.IsDetector.def'

added theorem CategoryTheory.IsDetector.def

deleted theorem CategoryTheory.IsSeparator.def'

added theorem CategoryTheory.IsSeparator.def

Modified Mathlib/CategoryTheory/Preadditive/Generator.lean

Modified Mathlib/CategoryTheory/Subterminal.lean

deleted theorem CategoryTheory.IsSubterminal.def'

added theorem CategoryTheory.IsSubterminal.def

Modified Mathlib/FieldTheory/AbelRuffini.lean

Modified Mathlib/FieldTheory/Finite/Basic.lean

Modified Mathlib/FieldTheory/Fixed.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean

Modified Mathlib/FieldTheory/IsSepClosed.lean

Modified Mathlib/FieldTheory/Normal.lean

Modified Mathlib/FieldTheory/Separable.lean

Modified Mathlib/FieldTheory/SplittingField/Construction.lean

Modified Mathlib/LinearAlgebra/Charpoly/Basic.lean

Modified Mathlib/LinearAlgebra/Matrix/Adjugate.lean

Modified Mathlib/LinearAlgebra/SModEq.lean

modified theorem SModEq.sub_mem

modified theorem SModEq.zero

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

Modified Mathlib/NumberTheory/Cyclotomic/Basic.lean

Modified Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean

Modified Mathlib/NumberTheory/FunctionField.lean

deleted theorem FunctionField.inftyValuedFqt.def'

added theorem FunctionField.inftyValuedFqt.def

deleted theorem FunctionField.valuedFqtInfty.def'

added theorem FunctionField.valuedFqtInfty.def

Modified Mathlib/NumberTheory/Liouville/Basic.lean

Modified Mathlib/NumberTheory/PrimesCongruentOne.lean

Modified Mathlib/Probability/Kernel/Invariance.lean

deleted theorem ProbabilityTheory.kernel.Invariant.def'

added theorem ProbabilityTheory.kernel.Invariant.def

Modified Mathlib/RingTheory/Discriminant.lean

Modified Mathlib/RingTheory/Henselian.lean

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean

Modified Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean

Modified Mathlib/RingTheory/Polynomial/Pochhammer.lean

Modified Mathlib/RingTheory/RootsOfUnity/Minpoly.lean

Modified Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean

Modified Mathlib/SetTheory/ZFC/Basic.lean

Modified Mathlib/Topology/Sober.lean

deleted theorem IsGenericPoint.def'

added theorem IsGenericPoint.def