# Zulip Chat Archive

## Stream: new members

### Topic: Coercions and liftings

#### Suryansh Shrivastava (Mar 25 2023 at 21:23):

I am getting stuck on lifting and coercions in lean3, is there a source to learn more about them?

#### Kevin Buzzard (Mar 25 2023 at 21:37):

You wait until you try Lean 4.

Are you specifically interested in the ins and outs of `has_lift_t`

and all that jazz (something I'm completely ignorant about, save for knowing that it's all changed in Lean 4 so there's no point learning about it anyway) or do you just want to know how to prove a goal involving integers when you have the corresponding hypothesis involving naturals?

#### Suryansh Shrivastava (Mar 26 2023 at 04:53):

Like when I was going through the definition of trece in finite fields, I didn't understand what the function of this symbol was:-⇑

The main theorem that I am looking at now is this :-

```
lemma trace_to_zmod_nondegenerate (F : Type*) [field F] [finite F] {a : F}
(ha : a ≠ 0) : ∃ b : F, algebra.trace (zmod (ring_char F)) F (a * b) ≠ 0 :=
begin
haveI : fact (ring_char F).prime := ⟨char_p.char_is_prime F _⟩,
have htr := trace_form_nondegenerate (zmod (ring_char F)) F a,
simp_rw [algebra.trace_form_apply] at htr,
by_contra' hf,
exact ha (htr hf),
end
```

#### Suryansh Shrivastava (Mar 26 2023 at 04:54):

but in the documentation, the same statement is given as :-

```
theorem finite_field.trace_to_zmod_nondegenerate (F : Type u_1) [field F] [finite F] {a : F} (ha : a ≠ 0) :
∃ (b : F), ⇑(algebra.trace (zmod (ring_char F)) F) (a * b) ≠ 0
```

#### Kevin Buzzard (Mar 26 2023 at 10:43):

It's the coercion from a function-like-thing (eg a group homomorphism, which is a function plus some axioms) to the underlying function

#### Suryansh Shrivastava (Mar 26 2023 at 13:34):

Okay, that makes sense, but we don't need to specify the coercion in our code?

#### Suryansh Shrivastava (Mar 26 2023 at 13:37):

or does lean generally decipher that for us?

#### Kevin Buzzard (Mar 26 2023 at 13:37):

Lean inserts it automatically if you write `f x`

where `f`

is a term which is not literally a function but you are attempting to evaluate it at `x`

. The moment Lean sees you putting a term next to another term in a kind of "I'm trying to apply a function to an input" way, if `f`

is not a function then the typeclass inference system will look for a coercion to a function. It's just like if you have `a : nat`

but then write `f a`

where `f`

is a function expecting a real number -- this time it will coerce `a`

from a natural to a real and you'l see `f `

\u a` where `

\u` is a little up-arrow this time representing a coercion from a term to another term.

#### Sky Wilshaw (Mar 26 2023 at 13:37):

Unfortunately, this process of elaboration isn't easily reversible. To generate the documentation, the elaborated code is "delaborated" back into human-readable stuff, but the delaborator isn't perfect!

#### Sky Wilshaw (Mar 26 2023 at 13:38):

It adds unnecessary things sometimes.

#### Kevin Buzzard (Mar 26 2023 at 13:38):

If the system finds a coercion to a function, it will apply the coercion and insert the relevant arrow; if it doesn't, you'll get an error of the form "I expected a function and got something else".

Yes, coercions are a good example where round-tripping is bad in Lean 3. If you cut and paste from the prettyprinter output and it doesn't compile because of an error under a coercion, just delete it; that usually does the trick.

Last updated: Dec 20 2023 at 11:08 UTC