BaseChange

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

Statistics

Metric	Count
Definitions	0
Theorems mem_subfield_of_mul_eq_one_of_mem_subfield_left, mem_subfield_of_mul_eq_one_of_mem_subfield_right	2
Total	2

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_subfield_of_mul_eq_one_of_mem_subfield_left 📖	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Subfield SetLike.instMembership Subfield.instSetLike	—	—	transpose_mul transpose_one transpose_apply mem_subfield_of_mul_eq_one_of_mem_subfield_right
mem_subfield_of_mul_eq_one_of_mem_subfield_right 📖	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Subfield SetLike.instMembership Subfield.instSetLike	—	—	nonempty_fintype IsUnit.of_mul_eq_one instIsDedekindFiniteMonoidOfIsStablyFiniteRing instIsStablyFiniteRingOfCommSemiring submatrix_mul_equiv submatrix_id_id RingHom.map_det AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass isUnit_iff_exists_inv instIsStablyFiniteRingSubtypeMem map_one submatrix_id_mul_left Equiv.symm_symm map_mul RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass mul_eq_one_comm_of_equiv one_mul mul_one

---

← Back to Index