## 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!