Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ideal.mem_span_singleton

Modification history

2023-01-09 10:12
src/ring_theory/ideal/basic.lean
feat(ring_theory/ideal/operations): add span_singleton_mul_left lemmas (#18056)
Modified ideal.mem_span_singletonView on Github →
2018-11-05 10:47
ring_theory/ideals.lean
feat(linear_algebra,ring_theory): refactoring modules (#456) …
Added ideal.mem_span_singletonView on Github →