theorem proved term proof

`vp_gcd`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  88theorem vp_gcd {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) (p : ℕ) :
  89    vp p (Nat.gcd a b) = min (vp p a) (vp p b) := by

proof body

Term-mode proof.

  90  simp only [vp]
  91  rw [Nat.factorization_gcd ha hb]
  92  rfl
  93
  94/-- The exponent of `p` in `lcm(a,b)` equals the maximum of the exponents.
  95For nonzero `a, b` and prime `p`. -/

depends on (7)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
vp in IndisputableMonolith.NumberTheory.Primes.Factorization decl_use