Changeset 351 for Deliverables/D4.1/Matita/Exponential.ma
 Timestamp:
 Dec 1, 2010, 4:30:46 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Exponential.ma
r268 r351 61 61 nqed. 62 62 63 (* 63 64 naxiom exponential_addition_exponential_multiplication: 64 65 ∀m, n, o: Nat. 65 66 (m^n) * (m^o) = m^(n + o). 66 67 67 (*68 68 nlemma exponential_exponential_multiplication: 69 69 ∀m, n, o: Nat.
Note: See TracChangeset
for help on using the changeset viewer.