Theorem Subsemiring.mem_iInf

Modification history

2025-12-16 07:12
Mathlib/Algebra/Ring/Subsemiring/Basic.lean
chore(Algebra): consistently tag `mem_sInf`, `mem_iInf`, `coe_sInf`, `coe_iInf` (#32887) …
Modified Subsemiring.mem_iInfView on Github →
2024-09-23 15:47
Mathlib/Algebra/Ring/Subsemiring/Basic.lean
feat: add `map_i[I]nf` for sub(semi)ring, subalgebra, subfield etc. (#15113) …
Added Subsemiring.mem_iInfView on Github →