Zulip Chat Archive

Stream: general

Topic: ring bug again?

Patrick Massot (Jul 31 2018 at 13:45):

example {α : Type*} [ring α] : ∀ a' b' a₁ b₁ a₂ b₂ : α,
    a₂*b₂ - a₁*b₁ = (a₂ - a₁)*b' + (a₂ - a₁)*(b₂ - b') + (b₂ - b₁)*a' + (b₂ - b₁)*(a₁ - a') :=
begin
  intros,
  ring,
  sorry
end

:disappointed:

Johan Commelin (Jul 31 2018 at 13:47):

comm_ring?

Patrick Massot (Jul 31 2018 at 13:47):

oh yes

Patrick Massot (Jul 31 2018 at 13:47):

Good observation

Johan Commelin (Jul 31 2018 at 13:48):

"In the following file, all rings are assumed commutative"

Patrick Massot (Jul 31 2018 at 13:48):

I blame Kevin who is always writing all rings are commutative

Kevin Buzzard (Jul 31 2018 at 14:19):

It's true by definition! It's a bug in Lean -- they missed commutativity out

Last updated: Dec 20 2023 at 11:08 UTC