Si R es un anillo ordenado, entonces ∀ a b ∈ R, a ≤ b → 0 ≤ b – a
Demostrar que si R es un anillo ordenado y a b ∈ R, entonces
|
1 |
a ≤ b → 0 ≤ b - a |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 |
import algebra.order.ring variables {R : Type*} [ordered_ring R] variables a b : R example : a ≤ b → 0 ≤ b - a := sorry |
Read More «Si R es un anillo ordenado, entonces ∀ a b ∈ R, a ≤ b → 0 ≤ b – a»