# Zulip Chat Archive

## Stream: general

### Topic: ring

#### Sebastien Gouezel (Nov 16 2019 at 10:10):

`ring`

just failed me on

lemma come_on_ring (x y : ℂ) : x * (2 : ℂ)⁻¹ = -((-1) * (2 : ℂ)⁻¹ * x) := begin ring, rw neg_neg, rw mul_comm end

First line should work but does not close the goal. Also, if you replace the line `rw mul_comm`

with `ring`

, it fails again but expands the definition of the inverse, which it didn't do in the first step.

#### Mario Carneiro (Nov 16 2019 at 10:13):

this works for me:

import tactic.ring variables {ℂ : Type} [linear_ordered_field ℂ] lemma come_on_ring (x y : ℂ) : x * (2 : ℂ)⁻¹ = -((-1) * (2 : ℂ)⁻¹ * x) := by ring1

#### Mario Carneiro (Nov 16 2019 at 10:14):

On further review, though, that typeclass is nonsense. Something requires a linear ordered semiring

#### Mario Carneiro (Nov 16 2019 at 10:15):

I think it is because it is trying to use `rat.cast`

to make sense of the one half

#### Sebastien Gouezel (Nov 16 2019 at 10:17):

Yes, `ℂ`

is not really ordered, but still it has characteristic `0`

...

#### Mario Carneiro (Nov 16 2019 at 10:20):

The culprit is `tactic.norm_num`

from core:

#eval tactic.norm_num `(1 / (2 : ℂ)) >>= tactic.trace -- failed to synthesize 'linear_ordered_semiring'

#### Mario Carneiro (Nov 16 2019 at 10:20):

mathlib has a `char_zero`

typeclass to address this, but we used `linear_ordered_field`

before that and the norm_num lemmas use it too

#### Mario Carneiro (Nov 16 2019 at 10:26):

It uses

#print norm_num.div_eq_div_helper -- theorem norm_num.div_eq_div_helper : ∀ {α : Type u} [_inst_1 : field α] (a b c d v : α), -- a * d = v → c * b = v → b ≠ 0 → d ≠ 0 → a / b = c / d

to prove equality of divisions by cross multiplication (causing a `2 ≠ 0`

subgoal), followed by

#print norm_num.nonzero_of_pos_helper -- theorem norm_num.nonzero_of_pos_helper : ∀ {α : Type u} [_inst_1 : linear_ordered_semiring α] (a : α), a > 0 → a ≠ 0

to deduce this from `2 > 0`

(at which point we are talking nonsense since there is no such order on complexes)

#### Mario Carneiro (Nov 16 2019 at 10:28):

In any case, you can solve the lemma like this:

lemma come_on_ring (x y : ℂ) : x * (2 : ℂ)⁻¹ = -((-1) * (2 : ℂ)⁻¹ * x) := by {generalize: (2 : ℂ)⁻¹ = a, ring}

#### Sebastien Gouezel (Nov 16 2019 at 10:29):

OK. Finally, in my more complex computation, I cheated by hiding `1/2`

from ring, with (a variant of)

lemma come_on_ring (x y : ℂ) : x * (2 : ℂ)⁻¹ = -((-1) * (2 : ℂ)⁻¹ * x) := begin set u : ℂ := (2 : ℂ)⁻¹, ring end

#### Sebastien Gouezel (Nov 16 2019 at 10:30):

Yes, it's essentially the same as your solution with `generalize`

.

Last updated: Dec 20 2023 at 11:08 UTC