Nuprl Lemma : real-det-req-matrix-det
∀n:ℕ. ∀M:ℕn ⟶ ℕn ⟶ ℝ. (|M| = |M|)
Proof
Definitions occuring in Statement :
real-det: |M|,
real-ring: real-ring(),
req: x = y,
real: ℝ,
int_seg: {i..j-},
nat: ℕ,
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
natural_number: $n,
matrix-det: |M|
Definitions unfolded in proof :
nat: ℕ,
uall: ∀[x:A]. B[x],
member: t ∈ T,
all: ∀x:A. B[x]
Latex:
\mforall{}n:\mBbbN{}. \mforall{}M:\mBbbN{}n {}\mrightarrow{} \mBbbN{}n {}\mrightarrow{} \mBbbR{}. (|M| = |M|)
Date html generated:
2020_05_20-PM-00_37_36
Last ObjectModification:
2019_12_28-AM-11_09_56
Theory : reals
Home
Index