Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subring.mem_pointwise_smul_iff_inv_smul_mem₀

Modification history

2021-11-23 07:23
src/ring_theory/subring/pointwise.lean
refactor(ring_theory/sub[semi]ring): move pointwise instances to their own file (#10347) …
Added subring.mem_pointwise_smul_iff_inv_smul_mem₀View on Github →