Commit 2023-10-03 08:56 56e89392

View on Github →

chore: move some code to Algebra.Module.Submodule.Lattice and add some comments (#7366)

Estimated changes

Modified Mathlib/Algebra/Module/Submodule/Lattice.lean

added theorem Submodule.mem_left_iff_eq_zero_of_disjoint

added theorem Submodule.mem_right_iff_eq_zero_of_disjoint

added theorem Submodule.nontrivial_iff

added theorem Submodule.subsingleton_iff

Modified Mathlib/LinearAlgebra/Basic.lean

deleted theorem Submodule.mem_left_iff_eq_zero_of_disjoint

deleted theorem Submodule.mem_right_iff_eq_zero_of_disjoint

deleted theorem Submodule.nontrivial_iff

deleted theorem Submodule.subsingleton_iff