Theorem MulSemiringAction.toRingEquiv_algEquiv

Modification history

2025-04-06 18:39
Mathlib/Algebra/Algebra/Equiv.lean
feat(NumberTheory): p-adic cyclotomic character (#21934)
Added MulSemiringAction.toRingEquiv_algEquivView on Github →