ax3_mul_assoc

Énoncé

∀ (a : ℝ) (b : ℝ) (c : ℝ), a * b * c = a * (b * c)

Le parenthésage d’un produit n’a pas d’importance.

Axiomes consommés

C’est un axiome : il est admis, pas démontré. Tout ce qui s’appuie dessus en hérite, et c’est précisément ce que cette bibliothèque rend visible.

• ax3_mul_assoc

Vocabulaire admis : myMul, ℝ — les déclarations qui nomment ℝ et ses opérations, communes à toute la bibliothèque.

Code

axiom ax3_mul_assoc : ∀ a b c : ℝ, (a * b) * c = a * (b * c)