← all areas

Namespace SetLike 4 theorems

• Degree-one rank bound from an injective Künneth map SetLike.GradedMonoid.rank_le_of_eq_bot_of_kunneth_injective 1 below · cited by 2 · depth 31
• Products of independent degree-one elements are non-zero SetLike.GradedMonoid.listProd_ne_zero_of_linearIndependent_of_kunneth_injective 0 below · cited by 3 · depth 32
• Primitive degree-two elements vanish under an injective Künneth map SetLike.GradedMonoid.eq_zero_of_mem_two_of_map_eq_add_of_kunneth_injective 1 below · cited by 3 · depth 35
• Degree two spanned by one product of degree-one elements SetLike.GradedMonoid.exists_forall_mem_two_eq_smul_mul_of_finrank_two_add_one_eq_of_kunneth_injective 2 below · cited by 1 · depth 38