## Stream: new members

### Topic: ring TC not working

#### Yakov Pechersky (Apr 07 2021 at 23:56):

Why does the second example here not work?

import tactic.ring_exp

example (a b : ℤ) : (a + b) * (a - b) = a ^ 2 - b ^ 2 :=
begin
ring_exp
end

example {R : Type*} [ring R] (a b : R) : (a + b) * (a - b) = a ^ 2 - b ^ 2 :=
begin
ring_exp
end


#### Yakov Pechersky (Apr 07 2021 at 23:56):

In widgets, clicking on ring gives no information.

#### Yakov Pechersky (Apr 07 2021 at 23:58):

Ah, I need comm_ring for the latter to work.

Last updated: May 18 2021 at 15:14 UTC