No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
134theorem polyCost_mul {f g : Polynomial F} (hf : f ≠ 0) (hg : g ≠ 0) :
135 polyCost (f * g) = polyCost f + polyCost g := by
proof body
Term-mode proof.
136 unfold polyCost
137 rw [normalizedFactors_mul hf hg]
138 rw [Multiset.map_add, Multiset.sum_add]
139
140/-! ## Cost on irreducibles and powers -/
141
142/-- For a monic irreducible polynomial `P`, the cost equals `J(‖P‖)`.
143 Mathlib's `normalizedFactors` returns the multiset of monic
144 irreducible factors. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (13)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
cost
in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
decl_use
-
cost
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
Cost
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
and
in IndisputableMonolith.NumberTheory.CirclePhaseLift
decl_use
-
polyCost
in IndisputableMonolith.NumberTheory.PrimeCostSpectrumPoly
decl_use
-
F
in IndisputableMonolith.Physics.AnchorPolicy
decl_use
-
F
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation
decl_use
-
F
in IndisputableMonolith.Pipelines
decl_use