Semiring mul_add

Stream: general

[Iocta]

What do I mean here?

import Mathlib
example {α : Type} [sr : Semiring α] (a x y : α): sr.mul a (sr.add x y) = sr.add (sr.mul a x) (sr.mul a y) := by
  sorry

[Yury G. Kudryashov]

Why do you use projections instead of notation? And what do you mean by your question?

[Iocta]

Why do you use projections instead of notation?

If I want to pass sr's mul operation into a function like map, how can I do it other than naming sr.mul? List.map (*) doesn't seem to work.

[Iocta]

And what do you mean by your question?

I thought simp [mul_add] would work, but it doesn't.

[Daniel Weber]

Iocta said:

Why do you use projections instead of notation?

If I want to pass sr's mul operation into a function like map, how can I do it other than naming sr.mul? List.map (*) doesn't seem to work.

def a : List Nat := [1, 2, 3]

#eval a.map (2 * ·)
-- [2, 4, 6]

[Daniel Weber]

example {α : Type} [sr : Semiring α] (a x y : α) :
    sr.mul a (sr.add x y) = sr.add (sr.mul a x) (sr.mul a y) := mul_add a x y

[Iocta]

What about this case, where it's inside a function?

example {α : Type} [Semiring α] (a x y : α): (fun x y => Mul.mul a (Add.add x y)) = (fun q r => Add.add (Mul.mul a x) (Mul.mul a y)) := by
  sorry

[Eric Wieser]

Again, you should not use Mul.mul and Add.add there

[Kevin Buzzard]

import Mathlib.Tactic

example {α : Type} [Semiring α] (a : α):
    (fun x y => a * (x + y)) = (fun q r => a * q + a * r) := by
  ext
  rw [mul_add]

(fixing the q,r error, using the usual notation)