Mathlib.Algebra.Expr

source

This file provides instances on x y : Q($α) such that x + y = q($x + $y).

x y : Q($α)

x + y = q($x + $y)

Porting note: This has been rewritten to use Qq instead of Expr.

Qq

Expr