Theorems · Theorem · linear algebra

Matrix.swap.congr_simp

∀ (R : Type u_1) {n : Type u_2} [inst : Zero R] [inst_1 : One R] {inst_2 : DecidableEq n} [inst_3 : DecidableEq n]
  (i i_1 : n),
  i = i_1 →
    ∀ (j j_1 : n),
      j = j_1 →
        ∀ (a a_1 : n), a = a_1 → ∀ (a_2 a_3 : n), a_2 = a_3 → Matrix.swap R i j a a_2 = Matrix.swap R i_1 j_1 a_1 a_3

Defined in: Mathlib.LinearAlgebra.Matrix.Swap
Cited by: 0 results in Mathlib
Foundations: Depth 22 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Zero One DecidableEq

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites1

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

Matrix.swapstatement and proof · cited by 19

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.