symm_mk — Mathlib

English

The symmetric of the constructed multiplicative isomorphism equals the multiplicative isomorphism built from the inverse of the base bijection.

Русский

Обратное к построенному мультипликативному изоморфизму равно изоморфизму, построенному из обратной биекции.

LaTeX

$$$\\mathrm{MulEquiv}.\\mathrm{symm}\\; (\\mathrm{mk}\\ f\\ h) = \\langle f^{-1}, (\\mathrm{mk}\\ f h).\\mathrm{symm\\_map\\_mul} \\rangle$$$

Lean4

@[to_additive (attr := simp)]
theorem symm_mk (f : M ≃ N) (h) : (MulEquiv.mk f h).symm = ⟨f.symm, (MulEquiv.mk f h).symm_map_mul⟩ :=
  rfl

Похожие утверждения