Mathlib v3 is deprecated. Go to Mathlib v4

Theorem algebra.pow_smul_mem_of_smul_subset_of_mem_adjoin

Modification history

2022-07-27 11:14
src/ring_theory/adjoin/basic.lean
feat(ring_theory/ring_hom/finite): Finite type is a local property (#15379)
Added algebra.pow_smul_mem_of_smul_subset_of_mem_adjoinView on Github →