Skip to content

Commit

Permalink
bump to nightly-2023-04-29-16
Browse files Browse the repository at this point in the history 
mathlib commit leanprover-community/mathlib@a4f99ea
  • Loading branch information
@leanprover-community-bot
leanprover-community-bot committed Apr 29, 2023
1 parent 7049eda commit 742d961
Show file tree
Hide file tree
Showing 5 changed files with 78 additions and 8 deletions.
24 changes: 24 additions & 0 deletions Mathbin/CategoryTheory/Abelian/Transfer.lean
View file

Large diffs are not rendered by default.

4 changes: 2 additions & 2 deletions Mathbin/LinearAlgebra/Dfinsupp.lean
View file
Expand Up @@ -803,7 +803,7 @@ omit dec_ι
lean 3 declaration is
forall {ι : Type.{u1}} {R : Type.{u2}} {N : Type.{u3}} [_inst_1 : Ring.{u2} R] [_inst_2 : AddCommGroup.{u3} N] [_inst_3 : Module.{u2, u3} R N (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} N _inst_2)] [_inst_4 : NoZeroSMulDivisors.{u2, u3} R N (MulZeroClass.toHasZero.{u2} R (NonUnitalNonAssocSemiring.toMulZeroClass.{u2} R (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u2} R (NonAssocRing.toNonUnitalNonAssocRing.{u2} R (Ring.toNonAssocRing.{u2} R _inst_1))))) (AddZeroClass.toHasZero.{u3} N (AddMonoid.toAddZeroClass.{u3} N (SubNegMonoid.toAddMonoid.{u3} N (AddGroup.toSubNegMonoid.{u3} N (AddCommGroup.toAddGroup.{u3} N _inst_2))))) (SMulZeroClass.toHasSmul.{u2, u3} R N (AddZeroClass.toHasZero.{u3} N (AddMonoid.toAddZeroClass.{u3} N (AddCommMonoid.toAddMonoid.{u3} N (AddCommGroup.toAddCommMonoid.{u3} N _inst_2)))) (SMulWithZero.toSmulZeroClass.{u2, u3} R N (MulZeroClass.toHasZero.{u2} R (MulZeroOneClass.toMulZeroClass.{u2} R (MonoidWithZero.toMulZeroOneClass.{u2} R (Semiring.toMonoidWithZero.{u2} R (Ring.toSemiring.{u2} R _inst_1))))) (AddZeroClass.toHasZero.{u3} N (AddMonoid.toAddZeroClass.{u3} N (AddCommMonoid.toAddMonoid.{u3} N (AddCommGroup.toAddCommMonoid.{u3} N _inst_2)))) (MulActionWithZero.toSMulWithZero.{u2, u3} R N (Semiring.toMonoidWithZero.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (AddZeroClass.toHasZero.{u3} N (AddMonoid.toAddZeroClass.{u3} N (AddCommMonoid.toAddMonoid.{u3} N (AddCommGroup.toAddCommMonoid.{u3} N _inst_2)))) (Module.toMulActionWithZero.{u2, u3} R N (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} N _inst_2) _inst_3))))] (p : ι -> (Submodule.{u2, u3} R N (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} N _inst_2) _inst_3)), (CompleteLattice.Independent.{succ u1, u3} ι (Submodule.{u2, u3} R N (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} N _inst_2) _inst_3) (Submodule.completeLattice.{u2, u3} R N (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} N _inst_2) _inst_3) p) -> (forall {v : ι -> N}, (forall (i : ι), Membership.Mem.{u3, u3} N (Submodule.{u2, u3} R N (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} N _inst_2) _inst_3) (SetLike.hasMem.{u3, u3} (Submodule.{u2, u3} R N (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} N _inst_2) _inst_3) N (Submodule.setLike.{u2, u3} R N (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} N _inst_2) _inst_3)) (v i) (p i)) -> (forall (i : ι), Ne.{succ u3} N (v i) (OfNat.ofNat.{u3} N 0 (OfNat.mk.{u3} N 0 (Zero.zero.{u3} N (AddZeroClass.toHasZero.{u3} N (AddMonoid.toAddZeroClass.{u3} N (SubNegMonoid.toAddMonoid.{u3} N (AddGroup.toSubNegMonoid.{u3} N (AddCommGroup.toAddGroup.{u3} N _inst_2))))))))) -> (LinearIndependent.{u1, u2, u3} ι R N v (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} N _inst_2) _inst_3))
but is expected to have type
forall {ι : Type.{u1}} {R : Type.{u3}} {N : Type.{u2}} [_inst_1 : DecidableEq.{succ u1} ι] [_inst_2 : Ring.{u3} R] [_inst_3 : AddCommGroup.{u2} N] [_inst_4 : Module.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_2) (AddCommGroup.toAddCommMonoid.{u2} N _inst_3)] [p : NoZeroSMulDivisors.{u3, u2} R N (MonoidWithZero.toZero.{u3} R (Semiring.toMonoidWithZero.{u3} R (Ring.toSemiring.{u3} R _inst_2))) (NegZeroClass.toZero.{u2} N (SubNegZeroMonoid.toNegZeroClass.{u2} N (SubtractionMonoid.toSubNegZeroMonoid.{u2} N (SubtractionCommMonoid.toSubtractionMonoid.{u2} N (AddCommGroup.toDivisionAddCommMonoid.{u2} N _inst_3))))) (SMulZeroClass.toSMul.{u3, u2} R N (NegZeroClass.toZero.{u2} N (SubNegZeroMonoid.toNegZeroClass.{u2} N (SubtractionMonoid.toSubNegZeroMonoid.{u2} N (SubtractionCommMonoid.toSubtractionMonoid.{u2} N (AddCommGroup.toDivisionAddCommMonoid.{u2} N _inst_3))))) (SMulWithZero.toSMulZeroClass.{u3, u2} R N (MonoidWithZero.toZero.{u3} R (Semiring.toMonoidWithZero.{u3} R (Ring.toSemiring.{u3} R _inst_2))) (NegZeroClass.toZero.{u2} N (SubNegZeroMonoid.toNegZeroClass.{u2} N (SubtractionMonoid.toSubNegZeroMonoid.{u2} N (SubtractionCommMonoid.toSubtractionMonoid.{u2} N (AddCommGroup.toDivisionAddCommMonoid.{u2} N _inst_3))))) (MulActionWithZero.toSMulWithZero.{u3, u2} R N (Semiring.toMonoidWithZero.{u3} R (Ring.toSemiring.{u3} R _inst_2)) (NegZeroClass.toZero.{u2} N (SubNegZeroMonoid.toNegZeroClass.{u2} N (SubtractionMonoid.toSubNegZeroMonoid.{u2} N (SubtractionCommMonoid.toSubtractionMonoid.{u2} N (AddCommGroup.toDivisionAddCommMonoid.{u2} N _inst_3))))) (Module.toMulActionWithZero.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_2) (AddCommGroup.toAddCommMonoid.{u2} N _inst_3) _inst_4))))] (hp : ι -> (Submodule.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_2) (AddCommGroup.toAddCommMonoid.{u2} N _inst_3) _inst_4)), (CompleteLattice.Independent.{succ u1, u2} ι (Submodule.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_2) (AddCommGroup.toAddCommMonoid.{u2} N _inst_3) _inst_4) (Submodule.completeLattice.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_2) (AddCommGroup.toAddCommMonoid.{u2} N _inst_3) _inst_4) hp) -> (forall {hv : ι -> N}, (forall (i : ι), Membership.mem.{u2, u2} N (Submodule.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_2) (AddCommGroup.toAddCommMonoid.{u2} N _inst_3) _inst_4) (SetLike.instMembership.{u2, u2} (Submodule.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_2) (AddCommGroup.toAddCommMonoid.{u2} N _inst_3) _inst_4) N (Submodule.setLike.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_2) (AddCommGroup.toAddCommMonoid.{u2} N _inst_3) _inst_4)) (hv i) (hp i)) -> (forall (i : ι), Ne.{succ u2} N (hv i) (OfNat.ofNat.{u2} N 0 (Zero.toOfNat0.{u2} N (NegZeroClass.toZero.{u2} N (SubNegZeroMonoid.toNegZeroClass.{u2} N (SubtractionMonoid.toSubNegZeroMonoid.{u2} N (SubtractionCommMonoid.toSubtractionMonoid.{u2} N (AddCommGroup.toDivisionAddCommMonoid.{u2} N _inst_3)))))))) -> (LinearIndependent.{u1, u3, u2} ι R N hv (Ring.toSemiring.{u3} R _inst_2) (AddCommGroup.toAddCommMonoid.{u2} N _inst_3) _inst_4))
forall {ι : Type.{u1}} {R : Type.{u3}} {N : Type.{u2}} [_inst_1 : Ring.{u3} R] [_inst_2 : AddCommGroup.{u2} N] [_inst_3 : Module.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} N _inst_2)] [_inst_4 : NoZeroSMulDivisors.{u3, u2} R N (MonoidWithZero.toZero.{u3} R (Semiring.toMonoidWithZero.{u3} R (Ring.toSemiring.{u3} R _inst_1))) (NegZeroClass.toZero.{u2} N (SubNegZeroMonoid.toNegZeroClass.{u2} N (SubtractionMonoid.toSubNegZeroMonoid.{u2} N (SubtractionCommMonoid.toSubtractionMonoid.{u2} N (AddCommGroup.toDivisionAddCommMonoid.{u2} N _inst_2))))) (SMulZeroClass.toSMul.{u3, u2} R N (NegZeroClass.toZero.{u2} N (SubNegZeroMonoid.toNegZeroClass.{u2} N (SubtractionMonoid.toSubNegZeroMonoid.{u2} N (SubtractionCommMonoid.toSubtractionMonoid.{u2} N (AddCommGroup.toDivisionAddCommMonoid.{u2} N _inst_2))))) (SMulWithZero.toSMulZeroClass.{u3, u2} R N (MonoidWithZero.toZero.{u3} R (Semiring.toMonoidWithZero.{u3} R (Ring.toSemiring.{u3} R _inst_1))) (NegZeroClass.toZero.{u2} N (SubNegZeroMonoid.toNegZeroClass.{u2} N (SubtractionMonoid.toSubNegZeroMonoid.{u2} N (SubtractionCommMonoid.toSubtractionMonoid.{u2} N (AddCommGroup.toDivisionAddCommMonoid.{u2} N _inst_2))))) (MulActionWithZero.toSMulWithZero.{u3, u2} R N (Semiring.toMonoidWithZero.{u3} R (Ring.toSemiring.{u3} R _inst_1)) (NegZeroClass.toZero.{u2} N (SubNegZeroMonoid.toNegZeroClass.{u2} N (SubtractionMonoid.toSubNegZeroMonoid.{u2} N (SubtractionCommMonoid.toSubtractionMonoid.{u2} N (AddCommGroup.toDivisionAddCommMonoid.{u2} N _inst_2))))) (Module.toMulActionWithZero.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} N _inst_2) _inst_3))))] (p : ι -> (Submodule.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} N _inst_2) _inst_3)), (CompleteLattice.Independent.{succ u1, u2} ι (Submodule.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} N _inst_2) _inst_3) (Submodule.completeLattice.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} N _inst_2) _inst_3) p) -> (forall {v : ι -> N}, (forall (i : ι), Membership.mem.{u2, u2} N (Submodule.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} N _inst_2) _inst_3) (SetLike.instMembership.{u2, u2} (Submodule.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} N _inst_2) _inst_3) N (Submodule.setLike.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} N _inst_2) _inst_3)) (v i) (p i)) -> (forall (i : ι), Ne.{succ u2} N (v i) (OfNat.ofNat.{u2} N 0 (Zero.toOfNat0.{u2} N (NegZeroClass.toZero.{u2} N (SubNegZeroMonoid.toNegZeroClass.{u2} N (SubtractionMonoid.toSubNegZeroMonoid.{u2} N (SubtractionCommMonoid.toSubtractionMonoid.{u2} N (AddCommGroup.toDivisionAddCommMonoid.{u2} N _inst_2)))))))) -> (LinearIndependent.{u1, u3, u2} ι R N v (Ring.toSemiring.{u3} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} N _inst_2) _inst_3))
Case conversion may be inaccurate. Consider using '#align complete_lattice.independent.linear_independent CompleteLattice.Independent.linearIndependentₓ'. -/
/-- If a family of submodules is `independent`, then a choice of nonzero vector from each submodule
forms a linearly independent family.
Expand Down Expand Up @@ -831,7 +831,7 @@ theorem Independent.linearIndependent [NoZeroSMulDivisors R N] (p : ι → Submo
lean 3 declaration is
forall {ι : Type.{u1}} {R : Type.{u2}} {N : Type.{u3}} [_inst_1 : Ring.{u2} R] [_inst_2 : AddCommGroup.{u3} N] [_inst_3 : Module.{u2, u3} R N (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} N _inst_2)] [_inst_4 : NoZeroSMulDivisors.{u2, u3} R N (MulZeroClass.toHasZero.{u2} R (NonUnitalNonAssocSemiring.toMulZeroClass.{u2} R (NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring.{u2} R (NonAssocRing.toNonUnitalNonAssocRing.{u2} R (Ring.toNonAssocRing.{u2} R _inst_1))))) (AddZeroClass.toHasZero.{u3} N (AddMonoid.toAddZeroClass.{u3} N (SubNegMonoid.toAddMonoid.{u3} N (AddGroup.toSubNegMonoid.{u3} N (AddCommGroup.toAddGroup.{u3} N _inst_2))))) (SMulZeroClass.toHasSmul.{u2, u3} R N (AddZeroClass.toHasZero.{u3} N (AddMonoid.toAddZeroClass.{u3} N (AddCommMonoid.toAddMonoid.{u3} N (AddCommGroup.toAddCommMonoid.{u3} N _inst_2)))) (SMulWithZero.toSmulZeroClass.{u2, u3} R N (MulZeroClass.toHasZero.{u2} R (MulZeroOneClass.toMulZeroClass.{u2} R (MonoidWithZero.toMulZeroOneClass.{u2} R (Semiring.toMonoidWithZero.{u2} R (Ring.toSemiring.{u2} R _inst_1))))) (AddZeroClass.toHasZero.{u3} N (AddMonoid.toAddZeroClass.{u3} N (AddCommMonoid.toAddMonoid.{u3} N (AddCommGroup.toAddCommMonoid.{u3} N _inst_2)))) (MulActionWithZero.toSMulWithZero.{u2, u3} R N (Semiring.toMonoidWithZero.{u2} R (Ring.toSemiring.{u2} R _inst_1)) (AddZeroClass.toHasZero.{u3} N (AddMonoid.toAddZeroClass.{u3} N (AddCommMonoid.toAddMonoid.{u3} N (AddCommGroup.toAddCommMonoid.{u3} N _inst_2)))) (Module.toMulActionWithZero.{u2, u3} R N (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} N _inst_2) _inst_3))))] {v : ι -> N}, (forall (i : ι), Ne.{succ u3} N (v i) (OfNat.ofNat.{u3} N 0 (OfNat.mk.{u3} N 0 (Zero.zero.{u3} N (AddZeroClass.toHasZero.{u3} N (AddMonoid.toAddZeroClass.{u3} N (SubNegMonoid.toAddMonoid.{u3} N (AddGroup.toSubNegMonoid.{u3} N (AddCommGroup.toAddGroup.{u3} N _inst_2))))))))) -> (Iff (CompleteLattice.Independent.{succ u1, u3} ι (Submodule.{u2, u3} R N (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} N _inst_2) _inst_3) (Submodule.completeLattice.{u2, u3} R N (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} N _inst_2) _inst_3) (fun (i : ι) => Submodule.span.{u2, u3} R N (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} N _inst_2) _inst_3 (Singleton.singleton.{u3, u3} N (Set.{u3} N) (Set.hasSingleton.{u3} N) (v i)))) (LinearIndependent.{u1, u2, u3} ι R N v (Ring.toSemiring.{u2} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} N _inst_2) _inst_3))
but is expected to have type
forall {ι : Type.{u1}} {R : Type.{u3}} {N : Type.{u2}} [_inst_1 : DecidableEq.{succ u1} ι] [_inst_2 : Ring.{u3} R] [_inst_3 : AddCommGroup.{u2} N] [_inst_4 : Module.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_2) (AddCommGroup.toAddCommMonoid.{u2} N _inst_3)] [v : NoZeroSMulDivisors.{u3, u2} R N (MonoidWithZero.toZero.{u3} R (Semiring.toMonoidWithZero.{u3} R (Ring.toSemiring.{u3} R _inst_2))) (NegZeroClass.toZero.{u2} N (SubNegZeroMonoid.toNegZeroClass.{u2} N (SubtractionMonoid.toSubNegZeroMonoid.{u2} N (SubtractionCommMonoid.toSubtractionMonoid.{u2} N (AddCommGroup.toDivisionAddCommMonoid.{u2} N _inst_3))))) (SMulZeroClass.toSMul.{u3, u2} R N (NegZeroClass.toZero.{u2} N (SubNegZeroMonoid.toNegZeroClass.{u2} N (SubtractionMonoid.toSubNegZeroMonoid.{u2} N (SubtractionCommMonoid.toSubtractionMonoid.{u2} N (AddCommGroup.toDivisionAddCommMonoid.{u2} N _inst_3))))) (SMulWithZero.toSMulZeroClass.{u3, u2} R N (MonoidWithZero.toZero.{u3} R (Semiring.toMonoidWithZero.{u3} R (Ring.toSemiring.{u3} R _inst_2))) (NegZeroClass.toZero.{u2} N (SubNegZeroMonoid.toNegZeroClass.{u2} N (SubtractionMonoid.toSubNegZeroMonoid.{u2} N (SubtractionCommMonoid.toSubtractionMonoid.{u2} N (AddCommGroup.toDivisionAddCommMonoid.{u2} N _inst_3))))) (MulActionWithZero.toSMulWithZero.{u3, u2} R N (Semiring.toMonoidWithZero.{u3} R (Ring.toSemiring.{u3} R _inst_2)) (NegZeroClass.toZero.{u2} N (SubNegZeroMonoid.toNegZeroClass.{u2} N (SubtractionMonoid.toSubNegZeroMonoid.{u2} N (SubtractionCommMonoid.toSubtractionMonoid.{u2} N (AddCommGroup.toDivisionAddCommMonoid.{u2} N _inst_3))))) (Module.toMulActionWithZero.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_2) (AddCommGroup.toAddCommMonoid.{u2} N _inst_3) _inst_4))))] {h_ne_zero : ι -> N}, (forall (i : ι), Ne.{succ u2} N (h_ne_zero i) (OfNat.ofNat.{u2} N 0 (Zero.toOfNat0.{u2} N (NegZeroClass.toZero.{u2} N (SubNegZeroMonoid.toNegZeroClass.{u2} N (SubtractionMonoid.toSubNegZeroMonoid.{u2} N (SubtractionCommMonoid.toSubtractionMonoid.{u2} N (AddCommGroup.toDivisionAddCommMonoid.{u2} N _inst_3)))))))) -> (Iff (CompleteLattice.Independent.{succ u1, u2} ι (Submodule.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_2) (AddCommGroup.toAddCommMonoid.{u2} N _inst_3) _inst_4) (Submodule.completeLattice.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_2) (AddCommGroup.toAddCommMonoid.{u2} N _inst_3) _inst_4) (fun (i : ι) => Submodule.span.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_2) (AddCommGroup.toAddCommMonoid.{u2} N _inst_3) _inst_4 (Singleton.singleton.{u2, u2} N (Set.{u2} N) (Set.instSingletonSet.{u2} N) (h_ne_zero i)))) (LinearIndependent.{u1, u3, u2} ι R N h_ne_zero (Ring.toSemiring.{u3} R _inst_2) (AddCommGroup.toAddCommMonoid.{u2} N _inst_3) _inst_4))
forall {ι : Type.{u1}} {R : Type.{u3}} {N : Type.{u2}} [_inst_1 : Ring.{u3} R] [_inst_2 : AddCommGroup.{u2} N] [_inst_3 : Module.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} N _inst_2)] [_inst_4 : NoZeroSMulDivisors.{u3, u2} R N (MonoidWithZero.toZero.{u3} R (Semiring.toMonoidWithZero.{u3} R (Ring.toSemiring.{u3} R _inst_1))) (NegZeroClass.toZero.{u2} N (SubNegZeroMonoid.toNegZeroClass.{u2} N (SubtractionMonoid.toSubNegZeroMonoid.{u2} N (SubtractionCommMonoid.toSubtractionMonoid.{u2} N (AddCommGroup.toDivisionAddCommMonoid.{u2} N _inst_2))))) (SMulZeroClass.toSMul.{u3, u2} R N (NegZeroClass.toZero.{u2} N (SubNegZeroMonoid.toNegZeroClass.{u2} N (SubtractionMonoid.toSubNegZeroMonoid.{u2} N (SubtractionCommMonoid.toSubtractionMonoid.{u2} N (AddCommGroup.toDivisionAddCommMonoid.{u2} N _inst_2))))) (SMulWithZero.toSMulZeroClass.{u3, u2} R N (MonoidWithZero.toZero.{u3} R (Semiring.toMonoidWithZero.{u3} R (Ring.toSemiring.{u3} R _inst_1))) (NegZeroClass.toZero.{u2} N (SubNegZeroMonoid.toNegZeroClass.{u2} N (SubtractionMonoid.toSubNegZeroMonoid.{u2} N (SubtractionCommMonoid.toSubtractionMonoid.{u2} N (AddCommGroup.toDivisionAddCommMonoid.{u2} N _inst_2))))) (MulActionWithZero.toSMulWithZero.{u3, u2} R N (Semiring.toMonoidWithZero.{u3} R (Ring.toSemiring.{u3} R _inst_1)) (NegZeroClass.toZero.{u2} N (SubNegZeroMonoid.toNegZeroClass.{u2} N (SubtractionMonoid.toSubNegZeroMonoid.{u2} N (SubtractionCommMonoid.toSubtractionMonoid.{u2} N (AddCommGroup.toDivisionAddCommMonoid.{u2} N _inst_2))))) (Module.toMulActionWithZero.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} N _inst_2) _inst_3))))] {v : ι -> N}, (forall (i : ι), Ne.{succ u2} N (v i) (OfNat.ofNat.{u2} N 0 (Zero.toOfNat0.{u2} N (NegZeroClass.toZero.{u2} N (SubNegZeroMonoid.toNegZeroClass.{u2} N (SubtractionMonoid.toSubNegZeroMonoid.{u2} N (SubtractionCommMonoid.toSubtractionMonoid.{u2} N (AddCommGroup.toDivisionAddCommMonoid.{u2} N _inst_2)))))))) -> (Iff (CompleteLattice.Independent.{succ u1, u2} ι (Submodule.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} N _inst_2) _inst_3) (Submodule.completeLattice.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} N _inst_2) _inst_3) (fun (i : ι) => Submodule.span.{u3, u2} R N (Ring.toSemiring.{u3} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} N _inst_2) _inst_3 (Singleton.singleton.{u2, u2} N (Set.{u2} N) (Set.instSingletonSet.{u2} N) (v i)))) (LinearIndependent.{u1, u3, u2} ι R N v (Ring.toSemiring.{u3} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} N _inst_2) _inst_3))
Case conversion may be inaccurate. Consider using '#align complete_lattice.independent_iff_linear_independent_of_ne_zero CompleteLattice.independent_iff_linearIndependent_of_ne_zeroₓ'. -/
theorem independent_iff_linearIndependent_of_ne_zero [NoZeroSMulDivisors R N] {v : ι → N}
(h_ne_zero : ∀ i, v i ≠ 0) : (Independent fun i => R ∙ v i) ↔ LinearIndependent R v :=
Expand Down

0 comments on commit 742d961

Please sign in to comment.