theorem Module.codim_iInf_ker_le_fintypeCard {K : Type u_1} {V : Type u_2} {ι : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : ι → V →ₗ[K] K} [Fintype ι] : finrank K V - (⨅ (i : ι), (f i).ker).finrank ≤ Fintype.card ι

theorem Module.codim_biInf_ker_le_finsetCard {K : Type u_1} {V : Type u_2} {ι : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {s : Finset ι} {f : ι → V →ₗ[K] K} : finrank K V - (⨅ i ∈ s, (f i).ker).finrank ≤ s.card