← all areas

Namespace QuotSMulTop 3 theorems

• Bases lift along a regular element of the maximal ideal QuotSMulTop.exists_basis_lift 2 below · cited by 2 · depth 32
• Lifting linear independence across M → M/xM for regular x QuotSMulTop.linearIndependent_of_quotientMk_linearIndependent 0 below · cited by 1 · depth 33
• Nakayama lifting of generators along M → M/xM QuotSMulTop.span_eq_top_of_span_quotientMk_eq_top 0 below · cited by 1 · depth 33