Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-05 11:06 c108ed47

View on Github →

feat(topology/algebra): add several lemmas (#13135)

  • add closure_smul, interior_smul, and closure_smul₀;
  • add is_open.mul_closure and is_open.closure_mul.

Estimated changes

added theorem closure_smul
added theorem closure_smul₀
modified def homeomorph.smul
added theorem interior_smul
added theorem is_open.closure_mul
added theorem is_open.mul_closure