En los anillos ordenados, {a ≤ b, 0 ≤ c} ⊢ ac ≤ bc
Demostrar con Lean4 que, en los anillos ordenados,
{a≤b,0≤c}⊢ac≤bc
Para ello, completar la siguiente teoría de Lean4:
Read More «En los anillos ordenados, {a ≤ b, 0 ≤ c} ⊢ ac ≤ bc»
Demostrar con Lean4 que, en los anillos ordenados,
{a≤b,0≤c}⊢ac≤bc
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Algebra.Order.Ring.Defs variable {R : Type _} [StrictOrderedRing R] variable (a b c : R) example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := by sorry |
Read More «En los anillos ordenados, {a ≤ b, 0 ≤ c} ⊢ ac ≤ bc»