ax4_mul_one

Énoncé

∀ (a : ℝ), a * 1 = a

Multiplier par un ne change rien.

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.

• ax4_mul_one

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

Code

axiom ax4_mul_one  : ∀ a : ℝ, a * 1 = a