Basic

📁 Source: Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Basic.lean

Statistics

Metric	Count
Definitions planeConformalMatrix	1
Theorems center_eq_range_scalar, center_eq_range_units, mem_center_iff_val_eq_scalar, mem_center_iff_val_mem_range_scalar, val_planeConformalMatrix	5
Total	6

Matrix

Definitions

Name	Category	Theorems
planeConformalMatrix 📖	CompOp	4 math math: toMatrix_rotation, ModularGroup.lcRow0Extend_symm_apply, ModularGroup.lcRow0Extend_apply, val_planeConformalMatrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
val_planeConformalMatrix 📖	mathematical	—	Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Fin.fintype planeConformalMatrix DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike of vecCons NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing vecEmpty	—	—

Matrix.GeneralLinearGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
center_eq_range_scalar 📖	mathematical	—	Subgroup.center Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MonoidHom.range Units scalar	—	Subgroup.ext isEmpty_or_nonempty Unique.instSubsingleton Matrix.subsingleton_of_empty_right mem_center_iff_val_mem_range_scalar Subgroup.inv_mem Matrix.diagonal_mul_diagonal mul_inv_cancel mul_comm
center_eq_range_units 📖	mathematical	—	Subgroup.center Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MonoidHom.range Units scalar	—	center_eq_range_scalar
mem_center_iff_val_eq_scalar 📖	mathematical	—	Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SetLike.instMembership Subgroup.instSetLike Subgroup.center Set Set.instMembership Set.range DFunLike.coe RingHom Semiring.toNonAssocSemiring Matrix.nonAssocSemiring RingHom.instFunLike Matrix.scalar Units.val	—	mem_center_iff_val_mem_range_scalar
mem_center_iff_val_mem_range_scalar 📖	mathematical	—	Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Subgroup Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring SetLike.instMembership Subgroup.instSetLike Subgroup.center Set Set.instMembership Set.range DFunLike.coe RingHom Semiring.toNonAssocSemiring Matrix.nonAssocSemiring RingHom.instFunLike Matrix.scalar Units.val	—	Matrix.mem_range_scalar_of_commute_transvectionStruct Matrix.TransvectionStruct.mul_inv Matrix.TransvectionStruct.inv_mul Subgroup.mem_center_iff Commute.symm Matrix.scalar_commute mul_comm

---

← Back to Index