mathlib3
da07a992 - feat(ring_theory/tensor_product): Range of `tensor_product.product_map` (#10882)

Commit

4 years ago

feat(ring_theory/tensor_product): Range of `tensor_product.product_map` (#10882) This PR proves `(product_map f g).range = f.range ⊔ g.range`.

Author

tb65536

Parents