Grace/Cumulus/Real/Power.g17

Open in Workbench Download source

Imports

Ring · Algebra.Group.Power

Declarations

• realPow def
• realPow.real theorem derivation
• realPow.zero theorem derivation
• realPow.succ theorem derivation
• realPow.add theorem derivation
• realPow.one theorem derivation
• realPow.zero_succ theorem derivation
• realPow.mul theorem derivation
• realPow.two theorem derivation

Source

1-- Natural powers of real numbers2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Real.Power8import Ring9import Algebra.Group.Power1011-- Real powers are the specialization of monoid powers to multiplication.12-- The heterogeneous notation records its type: Real × Nat → Real.13def realPow (A : Real, n : Nat) : Real :=14  monoidPow(realMul, realOne, A, n)1516notation infixr 80 "^" => realPow for Real, Nat1718theorem realPow.real (A : Real, n : Nat)19  shows Real(A ^ n)20proof21  have typedA : Real(A) by typecheck22  unfold realPow23  have closed := monoidPow.closed at24    ℝ, realMul, realOne, A, n with realMul.monoid, typedA25  exact closed2627theorem realPow.zero (A : Real)28  shows A ^ 0 = 129proof30  unfold realPow31  exact monoidPow.zero3233theorem realPow.succ (A : Real, n : Nat)34  shows A ^ succ(n) = A * A ^ n35proof36  unfold realPow37  exact monoidPow.succ with assumption3839theorem realPow.add (A : Real, m n : Nat)40  shows A ^ (m + n) = A ^ m * A ^ n41proof42  have typedA : Real(A) by typecheck43  unfold Real at typedA44  unfold realPow45  exact monoidPow.add with realMul.monoid, typedA4647theorem realPow.one (n : Nat)48  shows (1:R) ^ n = (1:R)49proof50  induction n51  | zero =>52    rw realPow.zero53    rfl54  | succ(k) using ih =>55    rw [realPow.succ, ih]56    ring5758theorem realPow.zero_succ (n : Nat)59  shows (0:R) ^ succ(n) = (0:R)60proof61  rw realPow.succ62  ring6364theorem realPow.mul (A B : Real, n : Nat)65  shows (A * B) ^ n = A ^ n * B ^ n66proof67  induction n68  | zero =>69    rw [realPow.zero, realPow.zero, realPow.zero]70    ring71  | succ(k) using ih =>72    rw [realPow.succ, realPow.succ, realPow.succ, ih]73    ring7475theorem realPow.two (A : Real)76  shows A ^ succ(succ(0)) = A * A77proof78  rw [realPow.succ, realPow.succ, realPow.zero]79  ring80