Stream: new members

Topic: Issue with add_smul: Field vs Semiring

Arien Malec (Dec 10 2023 at 21:09):

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✝: 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 (Dec 10 2023 at 21:12):

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 (Dec 10 2023 at 21:14):

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

Richard Copley (Dec 10 2023 at 21:21):

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)


Same issue...

Arien Malec (Dec 10 2023 at 21:24):

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

Ruben Van de Velde (Dec 10 2023 at 21:25):

add_smul does not expect a type, it expects two values

Ruben Van de Velde (Dec 10 2023 at 21:26):

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 (Dec 10 2023 at 21:28):

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

Eric Wieser (Dec 10 2023 at 21:40):

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

Last updated: Dec 20 2023 at 11:08 UTC