Zulip Chat Archive

Stream: general

Topic: ring vs ring_nf


Damiano Testa (Jun 24 2021 at 14:50):

Another quiz: I was somewhat surprised by Lean's conclusions with the three proofs below.

Can you guess whether Lean accepts them, discards them, or does a mix?

import tactic.ring

lemma zero_le_zero_mul_zero1 : 0  0 * 0 := by ring
lemma zero_le_zero_mul_zero2 : 0  0 * 0 := by ring_nf
lemma zero_le_zero_mul_zero3 : 0  0 * 0 := le_of_eq (by ring)

Last updated: Dec 20 2023 at 11:08 UTC