Theorem Algebra.iInf_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.iInf_toSubsemiringView on Github →