Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subalgebra.mem_of_span_eq_top_of_smul_pow_mem

Modification history

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