Integer

📁 Source: Mathlib/LinearAlgebra/Matrix/Integer.lean

Statistics

Metric	Count
Definitions den, num	2
Theorems den_dvd_iff, den_intCast, den_map_intCast, den_map_natCast, den_natCast, den_ne_zero, den_neg, den_ofNat, den_one, den_transpose, den_zero, inv_denom_smul_num, map_mul_intCast, map_mul_natCast, map_mul_ratCast, num_div_den, num_eq_zero_iff, num_intCast, num_map_intCast, num_map_natCast, num_natCast, num_neg, num_ofNat, num_one, num_transpose, num_zero	26
Total	28

Matrix

Definitions

Name	Category	Theorems
den 📖	CompOp	12 math math: inv_denom_smul_num, den_zero, den_transpose, den_dvd_iff, den_map_intCast, den_map_natCast, num_div_den, den_intCast, den_one, den_ofNat, den_neg, den_natCast
num 📖	CompOp	12 math math: num_transpose, inv_denom_smul_num, num_neg, num_zero, num_map_intCast, num_map_natCast, num_ofNat, num_natCast, num_div_den, num_one, num_intCast, num_eq_zero_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
den_dvd_iff 📖	mathematical	—	den	—	—
den_intCast 📖	mathematical	—	den Matrix instIntCastOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Rat.commRing	—	diagonal_map Int.cast_zero den_map_intCast
den_map_intCast 📖	mathematical	—	den map	—	Unique.instSubsingleton
den_map_natCast 📖	mathematical	—	den map	—	Unique.instSubsingleton
den_natCast 📖	mathematical	—	den Matrix instNatCastOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Rat.commRing	—	diagonal_map Nat.cast_zero den_map_natCast
den_ne_zero 📖	—	—	—	—	Nat.instNontrivial
den_neg 📖	mathematical	—	den Matrix neg	—	eq_of_forall_dvd Nat.instIsCancelMulZero Unique.instSubsingleton
den_ofNat 📖	mathematical	—	den	—	den_natCast
den_one 📖	mathematical	—	den Matrix one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Rat.commRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Rat.instDivisionRing	—	den_natCast
den_transpose 📖	mathematical	—	den transpose	—	eq_of_forall_dvd Nat.instIsCancelMulZero Unique.instSubsingleton
den_zero 📖	mathematical	—	den Matrix zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Rat.commRing	—	den_map_natCast
inv_denom_smul_num 📖	mathematical	—	Matrix smul Algebra.toSMul Rat.commSemiring CommSemiring.toSemiring Algebra.id den map num	—	ext num_div_den div_eq_inv_mul
map_mul_intCast 📖	mathematical	—	map Matrix instHMulOfFintypeOfMulOfAddCommMonoid Int.instAddCommMonoid AddGroupWithOne.toIntCast AddCommGroupWithOne.toAddGroupWithOne NonAssocRing.toAddCommGroupWithOne instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing NonUnitalNonAssocSemiring.toAddCommMonoid	—	map_mul RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass
map_mul_natCast 📖	mathematical	—	map Matrix instHMulOfFintypeOfMulOfAddCommMonoid Nat.instAddCommMonoid AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid	—	map_mul RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass
map_mul_ratCast 📖	mathematical	—	map Matrix instHMulOfFintypeOfMulOfAddCommMonoid Rat.addCommMonoid DivisionRing.toRatCast instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing NonUnitalNonAssocSemiring.toAddCommMonoid	—	map_mul RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass
num_div_den 📖	mathematical	—	num den	—	den_dvd_iff dvd_refl num.eq_1 map_apply smul_apply smul_eq_mul mul_comm div_eq_iff Nat.cast_ne_zero Rat.instCharZero den_ne_zero Nat.cast_mul mul_assoc Rat.mul_den_eq_num Int.cast_natCast Int.cast_mul
num_eq_zero_iff 📖	mathematical	—	num Matrix zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing Rat.commRing	—	IsDomain.to_noZeroDivisors Rat.isDomain Rat.instCharZero den_ne_zero
num_intCast 📖	mathematical	—	num Matrix instIntCastOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Rat.commRing Int.instCommRing	—	diagonal_map Int.cast_zero num_map_intCast
num_map_intCast 📖	mathematical	—	num map	—	den_map_intCast Nat.cast_one one_smul map_map map_id'
num_map_natCast 📖	mathematical	—	num map	—	den_map_natCast Nat.cast_one one_smul map_map
num_natCast 📖	mathematical	—	num Matrix instNatCastOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Rat.commRing Int.instCommRing	—	diagonal_map Nat.cast_zero num_map_natCast
num_neg 📖	mathematical	—	num Matrix neg	—	ext den_neg smul_neg
num_ofNat 📖	mathematical	—	num Matrix instNatCastOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	num_natCast
num_one 📖	mathematical	—	num Matrix one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Rat.commRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Rat.instDivisionRing Int.instCommRing Int.instRing	—	num_natCast
num_transpose 📖	mathematical	—	num transpose	—	ext den_transpose
num_zero 📖	mathematical	—	num Matrix zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Rat.commRing Int.instCommRing	—	num_map_natCast

---

← Back to Index