Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-20 11:48 ba282349

View on Github →

feat(algebra/pointwise): more lemmas about pointwise actions (#9226) This:

  • Primes the existing lemmas about group_with_zero and adds their group counterparts
  • Adds:
    • smul_mem_smul_set_iff
    • set_smul_subset_set_smul_iff
    • set_smul_subset_iff
    • subset_set_smul_iff
  • Generalizes zero_smul_set to take weaker typeclasses

Estimated changes

added theorem mem_inv_smul_set_iff'
modified theorem mem_inv_smul_set_iff
modified theorem preimage_smul'
modified theorem preimage_smul
added theorem set_smul_subset_iff'
added theorem set_smul_subset_iff
added theorem smul_mem_smul_set_iff'
added theorem smul_mem_smul_set_iff
added theorem subset_set_smul_iff'
added theorem subset_set_smul_iff
modified theorem zero_smul_set