Si R es un anillo ordenado y a, b ∈ R, entonces 0 ≤ b – a → a ≤ b
Demostrar que si R es un anillo ordenado y a, b ∈ R, entonces
|
1 |
0 ≤ b - a → a ≤ b |
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 : 0 ≤ b - a → a ≤ b := sorry |
Read More «Si R es un anillo ordenado y a, b ∈ R, entonces 0 ≤ b – a → a ≤ b»