Commit 2023-02-06 00:44 089682c5

View on Github →

feat: port Algebra.CharZero.Quotient (#2022)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/CharZero/Quotient.lean

added theorem AddSubgroup.nsmul_mem_zmultiples_iff_exists_sub_div

added theorem AddSubgroup.zsmul_mem_zmultiples_iff_exists_sub_div

added theorem quotientAddGroup.zmultiples_nsmul_eq_nsmul_iff

added theorem quotientAddGroup.zmultiples_zsmul_eq_zsmul_iff