Theorem Algebra.iSup_toSubsemiring

Modification history

2024-10-16 04:43
Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
feat: add `[s|i]sup_toXXX` for intermediate fields and subalgebras (#15088) …
Added Algebra.iSup_toSubsemiringView on Github →