# Zulip Chat Archive

## Stream: new members

### Topic: Why is [field F] not an implicit argument?

#### Martin C. Martin (Aug 01 2023 at 20:11):

I'm re-implementing vector spaces and sub spaces. In mathlib's `submodule`

, we show that a submodule is a module. I'm trying to do the same thing, but running into a difference that I don't understand.

`#check submodule.module' `

: returns

```
Π (p : submodule ?M_2 ?M_3) [_inst_3 : semiring ?M_1] [_inst_4 : has_smul ?M_1 ?M_2] [_inst_5 : module ?M_1 ?M_3]
[_inst_6 : is_scalar_tower ?M_1 ?M_2 ?M_3], module ?M_1 ↥p
```

i.e. there are implicit arguments for all the algebraic structure objects. However, in my code, I just get:

`#check #check subspace.vector_space'`

returns

`subspace.vector_space' : Π (q : subspace ?M_1 ?M_2), vector_space ?M_1 ↥q`

In particular, there's no requirement for `[field ?M_1]`

.

Why doesn't that show up?

My #mwe, sorry it's so long:

```
import algebra.module.basic
import data.set_like.basic
set_option old_structure_cmd true
namespace LADR
@[ext]
class vector_space (F : Type*) (V : Type*) [field F] [add_comm_group V]
extends has_smul F V :=
(smul_assoc : ∀ a b : F, ∀ v : V, (a * b) • v = a • (b • v))
(mul_ident : ∀ v : V, (1 : F) • v = v)
(left_distrib : ∀ a : F, ∀ u v : V, a • (u + v) = (a • u) + (a • v))
(right_distrib : ∀ a b :F, ∀ v : V, (a + b) • v = (a • v) + (b • v))
variables {F : Type*} [field F]
namespace vector_space
variables {V : Type*} [add_comm_group V] [vector_space F V]
theorem neg_one_smul_is_neg {v : V} : (-1 : F) • v = - v := sorry
end vector_space
structure add_comm_subgroup (V : Type*) [add_comm_group V] :=
(carrier : set V)
(add_mem' : ∀ {u v : V}, u ∈ carrier → v ∈ carrier → u + v ∈ carrier)
(zero_mem' : (0 : V) ∈ carrier)
-- ********** BOILERPLATE FOR set_like **********
namespace add_comm_subgroup
variables {V : Type*} [add_comm_group V] {v : V}
instance : set_like (add_comm_subgroup V) V :=
⟨ add_comm_subgroup.carrier, λ p q h, by cases p; cases q; congr'⟩
@[simp] lemma mem_carrier {p : add_comm_subgroup V} : v ∈ p.carrier ↔ v ∈ (p : set V) := iff.rfl
@[ext] theorem ext {p q : add_comm_subgroup V} (h : ∀ v, v ∈ p ↔ v ∈ q) : p = q := set_like.ext h
end add_comm_subgroup
-- ********** BOILERPLATE ENDS **********
structure subspace (F : Type*) (V : Type*)
[field F] [add_comm_group V] [vector_space F V] extends add_comm_subgroup V :=
(smul_mem' : ∀ (c : F) {v : V}, v ∈ carrier → c • v ∈ carrier )
namespace subspace
variables {V : Type*} [add_comm_group V] [vector_space F V]
variable {v : V}
-- ********** BOILERPLATE FOR set_like **********
instance : set_like (subspace F V) V :=
⟨subspace.carrier, λ p q h, by cases p; cases q; congr'⟩
@[simp] lemma mem_carrier {p : subspace F V} : v ∈ p.carrier ↔ v ∈ (p : set V) := iff.rfl
@[ext] theorem ext {p q : subspace F V} (h : ∀ v, v ∈ p ↔ v ∈ q) : p = q := set_like.ext h
-- ********** BOILERPLATE ENDS **********
variables (p : subspace F V)
instance fooblah : add_comm_group p := {
add := λ u v, ⟨ u.1 + v.1, by { apply p.add_mem', simp, simp} ⟩,
zero := ⟨0, p.zero_mem'⟩,
neg := λ v, ⟨-v.1, by { rw ← @vector_space.neg_one_smul_is_neg F _ V, apply p.smul_mem', simp }⟩,
add_comm := sorry,
add_assoc := sorry,
add_zero := sorry,
zero_add := sorry,
add_left_neg := sorry,
}
instance vector_space' : vector_space F p := {
smul := λ s v, ⟨ s • v.1, by { apply p.smul_mem', simp} ⟩,
smul_assoc := by {intros, simp, apply vector_space.smul_assoc},
mul_ident := by {intros, ext, simp, rw vector_space.mul_ident},
left_distrib := sorry,
right_distrib := sorry
}
#check subspace.vector_space'
instance : vector_space F p := p.vector_space'
end subspace
end LADR
```

#### Eric Wieser (Aug 01 2023 at 22:37):

You want `#check @subspace.vector_space'`

not `#check subspace.vector_space'`

#### Eric Wieser (Aug 01 2023 at 22:37):

Note Lean 4 does this automatically for you

#### Martin C. Martin (Aug 02 2023 at 00:00):

Eric Wieser said:

You want

`#check @subspace.vector_space'`

not`#check subspace.vector_space'`

Ah, thanks! But why does `[_inst_3 : semiring ?M_1] `

show up for `module'`

, without the @, but the equivalent not show up for `vector_space'`

? Just some quirk of the printing logic, or is there something deeper, like the difference between `variable`

and `constant`

?

#### Scott Morrison (Aug 02 2023 at 00:57):

Could I ask why you're doing this in Lean 3 rather than Lean 4?

#### Eric Wieser (Aug 02 2023 at 01:34):

It shows up for one but not the other because one uses `(p : submodule ...)`

and the other uses `{p : submodule ...}`

#### Eric Wieser (Aug 02 2023 at 01:35):

Roughly speaking, Lean fills in `{}`

and `[]`

until it hits the first `()`

argument. `@`

tells it not to do this.

#### Martin C. Martin (Aug 02 2023 at 11:02):

Eric Wieser said:

Roughly speaking, Lean fills in

`{}`

and`[]`

until it hits the first`()`

argument.`@`

tells it not to do this.

Oh interesting! Is this documented somewhere? Such as the Lean reference manual?

#### Martin C. Martin (Aug 02 2023 at 17:36):

Scott Morrison said:

Could I ask why you're doing this in Lean 3 rather than Lean 4?

Which one is considered the best to use for new projects these days? How far along is the Lean 4 port of mathlib? Do enough people here on Zulip know about Lean 4 and can help?

#### Kyle Miller (Aug 02 2023 at 17:40):

All of mathlib is ported as of a couple weeks ago, and mathlib4 is now accepting contributions of new material

#### Martin C. Martin (Aug 02 2023 at 17:43):

Awesome! I guess I'll switch to that. Is there a document on the difference, "Lean 4 for the Lean 3 worker"?

#### Peter Hansen (Aug 02 2023 at 17:47):

Martin C. Martin said:

Awesome! I guess I'll switch to that. Is there a document on the difference, "Lean 4 for the Lean 3 worker"?

Maybe this https://leanprover.github.io/lean4/doc/lean3changes.html

#### Pedro Sánchez Terraf (Aug 02 2023 at 17:48):

Martin C. Martin said:

Awesome! I guess I'll switch to that. Is there a document on the difference, "Lean 4 for the Lean 3 worker"?

And the Lean 4 survival guide for Lean 3 users.

#### Martin C. Martin (Aug 02 2023 at 18:41):

How long before we start porting mathlib to Lean 5? :wink:

#### Ruben Van de Velde (Aug 02 2023 at 18:45):

Do you want to give people nightmares?

#### Martin C. Martin (Aug 02 2023 at 18:55):

Is there a tool for converting Lean 3 projects to Lean 4, like Python's 2to3?

#### Kyle Miller (Aug 02 2023 at 19:06):

Yes, you can use mathport (the same tool that helped drive the mathlib port). I haven't used it myself yet, but I've seen these instructions: https://github.com/leanprover-community/mathport/blob/master/Oneshot/README.md

#### Scott Morrison (Aug 03 2023 at 03:49):

That link is for porting single files at a time. If you'd like to try a whole project (it's been done twice to my knowledge so far, besides mathlib) see that main mathport README.

Last updated: Dec 20 2023 at 11:08 UTC