Def AlgEquiv.prodCongr

Modification history

2025-07-05 05:16

Mathlib/Algebra/Algebra/Prod.lean

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

Added AlgEquiv.prodCongr View on Github →