Theorem AlgEquiv.funUnique_symm_apply

Modification history

2025-07-05 05:16

Mathlib/Algebra/Algebra/Pi.lean

feat(Algebra/Pi): add various `AlgEquiv`s and `RingEquiv`s (#24520) …

Added AlgEquiv.funUnique_symm_apply View on Github →