Theorem RestrictedProduct.range_coe_principal
Modification history
2025-06-10 22:59
Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean
chore: split Mathlib/Topology/Algebra/RestrictedProduct (#25558) …
Modified RestrictedProduct.range_coe_principalView on Github →