has_smul ℚ k for field k

Stream: Is there code for X?

[Winston Yin]

Would it be meaningful to define the action of the rationals on any field k? For example, λ q c, if q.num = 0 then 0 else q.num • c * c / (q.denom • c)

[Violeta Hernández]

What if the field has finite characteristic?

[Violeta Hernández]

Might still work, I don't know, but you might end up with some perhaps unexpected divisions by zero

[Eric Wieser]

I guess you want more than docs#algebra_rat

[Eric Wieser]

I think you could prove that q.num • c * c / (q.denom • c) = q • c in char zero (where the RHS is algebra_rat)

[Kevin Buzzard]

Why add a non-mathematically-meaningful "action"? In characteristic p this can't be mathematically sensible.

[Damiano Testa]

Also, while I agree with Kevin that this does not seem like a good idea, why the case split?

import data.rat.defs

variables {k : Type*} [field k]

def mm (k : Type*) [field k]: ℚ → k → k :=
λ q c, if q.num = 0 then 0 else q.num • c * c / (q.denom • c)

def smm (k : Type*) [field k]: ℚ → k → k :=
λ q c, q.num • c * c / (q.denom • c)

example {k : Type*} [field k] : mm k = smm k :=
begin
  funext,
  unfold mm,
  unfold smm,
  split_ifs,
  simp [h],
end