Issue with `add_smul`: Field vs Semiring

Stream: new members

[Arien Malec]

One of the Axler problems is to show that "the additive inverse condition can be replaced with the condition that
0𝑣 = 0 for all 𝑣 ∈ 𝑉", which wants to proceed by showing that v-v = 1• v + -1 • v = (1 + -1) • v = 0 • v = 0

In:

import Mathlib.Algebra.Field.Basic
import Mathlib.Algebra.Module.Basic


variable [Field F] [AddCommGroup V] [Module F V]

example: ∀(v: V), (0: F)•v = 0 → ∃w, v + w = 0 := fun v h => by
  use ((-1: F) • v)
  rw [←one_smul F v, smul_comm, one_smul F ((-1: F) • v), ← add_smul F]

I get an odd error at add_smul

F: Type ?u.538
V: Type ?u.541
inst✝²: Field F
inst✝¹: AddCommGroup V
inst✝: Module F V
v: V
h: 0 • v = 0
⊢ 1 • v + -1 • v = 0
All Messages (2)
Scratch.lean:10:53
failed to synthesize instance
  Semiring (Type ?u.538)

Which is confusing because Field?

[Richard Copley]

add_mul's first explicit argument r should be of type R, where Semiring R is known to be true. Here you provide F, which is of type Type ?u.538 ...

[Arien Malec]

Right but F: Type ?u.538 and Field: F? and Field extend CommRing which extends Ring which extends Semiring?

[Richard Copley]

Sure. But you need an r : F, not an r : Type ?u.538.

Anyway. The real problem is that those 0s and 1s and -1s you're seeing aren't of type F.
Try

example (v : V) (h : (0 : F) • v = 0) : ∃ w, v + w = 0 := by
  use ((-1 : F) • v)

[Arien Malec]

Same issue...

[Arien Malec]

I updated the code to make all the things explicit..

[Ruben Van de Velde]

add_smul does not expect a type, it expects two values

[Ruben Van de Velde]

This could be seen as inconsistent with one_smul, but I guess there's no value you could pass which lean could derive the type from

[Arien Malec]

I was recently grumping that the foo_smul theorems require an explicit R and just now got used to it :-)

[Eric Wieser]

It's only the ones that don't take an explicit r : R which instead take an R : Type _, and this is deliberate