Commit 2023-04-20 11:28 a0ec9596

View on Github →

feat: port LinearAlgebra.FreeModule.PID (#3434)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/FreeModule/PID.lean

added structure Basis.SmithNormalForm

added theorem Ideal.exists_smith_normal_form

added theorem Ideal.selfBasis_def

added theorem Ideal.smithCoeffs_ne_zero

added theorem LinearIndependent.restrict_scalars_algebras

added theorem Module.free_of_finite_type_torsion_free'

added theorem Module.free_of_finite_type_torsion_free

added theorem Submodule.basisOfPid_bot

added theorem Submodule.basis_of_pid_aux

added theorem Submodule.exists_smith_normal_form_of_le

added theorem Submodule.nonempty_basis_of_pid

added theorem dvd_generator_iff

added theorem eq_bot_of_generator_maximal_map_eq_zero

added theorem eq_bot_of_generator_maximal_submoduleImage_eq_zero

added theorem generator_maximal_submoduleImage_dvd