mulEquivOfQuotient_symm_monoidOf — Mathlib

English

The symmetric equality respects mk for monoidOf and localization through the isomorphism.

Русский

Симметрическое равенство учитывает mk для monoidOf и локализации через изоморфизм.

LaTeX

$$$(mulEquivOfQuotient f).symm (f x) = monoidOf S x$$$

Lean4

@[to_additive (attr := simp)]
theorem mulEquivOfQuotient_symm_monoidOf (x) : (mulEquivOfQuotient f).symm (f x) = monoidOf S x :=
  f.lift_eq (monoidOf S).map_units _

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