ext — Mathlib

English

Extensionality principle for FixedDetMatrix: two entries equal implies equality of the fixed determinant matrices.

Русский

Принцип экстенсиональности для FixedDetMatrix: равенство всех соответствующих элементов означает равенство двух фиксированных детерминантных матриц.

LaTeX

$$$A = B$ if and only if $A_{ij} = B_{ij}$ for all i,j.$$

Lean4

@[ext]
theorem ext {m : R} {A B : FixedDetMatrix n R m} (h : ∀ i j, A.1 i j = B.1 i j) : A = B :=
  by
  apply ext'
  ext i j
  apply h

Похожие утверждения