Theorems · Theorem · linear algebra

Matrix.mul_eq_one_comm_of_card_eq

∀ (m : Type u_10) (n : Type u_11) (R : Type u_12) [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : Fintype n]
  [inst_3 : DecidableEq n] [inst_4 : MulOne R] [inst_5 : AddCommMonoid R] [IsStablyFiniteRing R] {A : Matrix m n R}
  {B : Matrix n m R}, Fintype.card m = Fintype.card n → (A * B = 1 ↔ B * A = 1)

Defined in: Mathlib.Data.Matrix.Mul
Cited by: 0 results in Mathlib
Foundations: Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Fintype DecidableEq Fintype DecidableEq MulOne AddCommMonoid IsStablyFiniteRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

AddCommMonoidstatement and proof · cited by 12,281
Fintypestatement and proof · cited by 7,736
Matrixstatement and proof · cited by 4,303
Fintype.cardstatement and proof · cited by 1,386
Nonempty.someproof · cited by 340
MulOnestatement and proof · cited by 65
Fintype.card_eqproof · cited by 19
IsStablyFiniteRingstatement and proof · cited by 11
Matrix.mul_eq_one_comm_of_equivproof · cited by 4

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.