Algebra.Field.Defs mathlib4#668

Stream: mathlib4

[Ruben Van de Velde]

Algebra.Field.Defs starts with

/-- The default definition of the coercion `(↑(a : ℚ) : K)` for a division ring `K`
is defined as `(a / b : K) = (a : K) * (b : K)⁻¹`.
Use `coe` instead of `rat.cast_rec` for better definitional behaviour.
-/
def Rat.castRec [HasLiftT ℕ K] [HasLiftT ℤ K] [Mul K] [Inv K] : ℚ → K
  | ⟨a, b, _, _⟩ => ↑a * (↑b)⁻¹

and I don't have a clue what the HasLiftT bits should be now. Is that something that needs to be imported from lean3port or do we need something else entirely?

[Scott Morrison]

No, this is waiting on the lift tactic, which Yury has been porting in https://github.com/leanprover-community/mathlib4/pull/723

[Scott Morrison]

He says that the code is working there, but I don't know what he's been testing it on as there are no tests in the PR.

[Eric Wieser]

docs#has_lift_t is nothing to do with tactic#lift, is it?

[Eric Wieser]

Are you thinking of docs#can_lift?

[Scott Morrison]

Oh, my mistake.

[Scott Morrison]

Can we just replace these with CoeT (or Coe)?

[Scott Morrison]

CoeTail seems to be right answer here.

[Scott Morrison]

Okay, I've almost finished with porting this file.

[Ruben Van de Velde]

Thanks! Looks like it wasn't too bad once you got past the coercions. One question though: shouldn't ratCastMk be ratCast_mk?

[Scott Morrison]

Ah, yes, you're right.

[Scott Morrison]

Fixed in mathlib4#808.