Theorem isEmbedding_prodMkLeft

Modification history

2025-06-12 05:16
Mathlib/Topology/Constructions/SumProd.lean
feat: is{Inducing,Embedding}_prodMkLeft (#25705) …
Added isEmbedding_prodMkLeftView on Github →