ax5_mul_inv

Énoncé

∀ (a : ℝ), a ≠ 0 → a * a⁻¹ = 1

Tout réel non nul a un inverse : leur produit vaut un.

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.

• ax5_mul_inv

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

Code

axiom ax5_mul_inv : ∀ a : ℝ, a ≠ 0 → a * a⁻¹ = 1

-- =============================================
-- AXIOME 6 : ORDRE
-- =============================================

-- Avec myLT on suppose l'existence de <
-- Lean définira automatiquement > par la suite