English
An equivalence e : α ≃ β gives a multiplicative equivalence α ≃* β by transporting multiplication along e.
Русский
Эквивалентность e : α ≃ β даёт мультипликативное эквивалентство α ≃* β путём переноса умножения вдоль e.
LaTeX
$$$$\text{There exists a multiplicative equivalence }\alpha \Cong_{\text{Mul}} \beta\text{ with underlying }e. $$$$
Lean4
/-- An equivalence `e : α ≃ β` gives a multiplicative equivalence `α ≃* β` where
the multiplicative structure on `α` is the one obtained by transporting a multiplicative structure
on `β` back along `e`. -/
@[to_additive /-- An equivalence `e : α ≃ β` gives an additive equivalence `α ≃+ β` where
the additive structure on `α` is the one obtained by transporting an additive structure
on `β` back along `e`. -/
]
def mulEquiv (e : α ≃ β) [Mul β] :
let _ := Equiv.mul e
α ≃* β :=
by
intros
exact { e with map_mul' := fun x y => by simp [mul_def] }
