Commit 2024-06-28 13:10 d2a5b412

View on Github →

chore: delay imports of Star (#14219)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Defs.lean

Modified Mathlib/Algebra/Algebra/Equiv.lean

Modified Mathlib/Algebra/Module/Equiv.lean

Modified Mathlib/Algebra/Module/LinearMap/Basic.lean

Created Mathlib/Algebra/Module/LinearMap/Star.lean

Modified Mathlib/Algebra/RingQuot.lean

deleted theorem RingQuot.Rel.star

deleted theorem RingQuot.star'_quot

deleted def RingQuot.starRing

Modified Mathlib/Algebra/Star/Basic.lean

deleted theorem star_nnratCast

deleted theorem star_ratCast

Modified Mathlib/Algebra/Star/CHSH.lean

Modified Mathlib/Algebra/Star/Module.lean

Created Mathlib/Algebra/Star/Rat.lean

added theorem star_nnratCast

added theorem star_ratCast

Created Mathlib/Algebra/Star/RingQuot.lean

added theorem RingQuot.Rel.star

added theorem RingQuot.star'_quot

added def RingQuot.starRing

Modified Mathlib/Algebra/Star/SelfAdjoint.lean

Modified Mathlib/Analysis/Analytic/Basic.lean

Modified Mathlib/Analysis/Calculus/LocalExtr/Polynomial.lean

Modified Mathlib/Analysis/InnerProductSpace/Dual.lean

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

Modified Mathlib/Analysis/Normed/Group/Quotient.lean

Modified Mathlib/Analysis/Normed/Order/UpperLower.lean

Modified Mathlib/Analysis/RCLike/Basic.lean

Modified Mathlib/Analysis/Seminorm.lean

Modified Mathlib/Analysis/SumOverResidueClass.lean

Modified Mathlib/Analysis/VonNeumannAlgebra/Basic.lean

Modified Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

Modified Mathlib/Data/Complex/Exponential.lean

Modified Mathlib/Data/Real/Sqrt.lean

Created Mathlib/Data/Real/Star.lean

Modified Mathlib/NumberTheory/PellMatiyasevic.lean

Modified Mathlib/Topology/Algebra/Module/Basic.lean

Modified Mathlib/Topology/Algebra/Module/Star.lean

Modified Mathlib/Topology/ContinuousFunction/ContinuousMapZero.lean

Modified Mathlib/Topology/ContinuousFunction/StarOrdered.lean

Modified scripts/noshake.json