I am currently studying linear algebra and have written the following definitions, yet I am unsure if they are correct. I am trying to write a more formal logical abstraction. I do not know if this is relevant, but it is an interesting approach.

Definition 1.5 (Row Echelon Form). For a matrix $A \in \mathbb{R}^{m \times n}$, $A$ is in row echelon form if:

Zero Rows at the Bottom: $\forall i \in \mathbb{N}_{\le m} \mid \bigwedge_{j=1}^n a_{ij}=0 \implies \bigwedge_{k=i+1}^m \bigwedge_{j=1}^n a_{kj}=0$

Leading Entry to the Right: $\forall i \in \mathbb{N}_{\le m} \; \exists j \in \mathbb{N}_{\le n} \mid a_{ij} \neq 0 \land \bigwedge_{k=i}^{m} a_{kj}=0 \implies \bigwedge_{k=1}^{j} a_{kj} = 0$

Definition 1.6 (Reduced Row Echelon Form). For a matrix $A \in \mathbb{R}^{m \times n}$, $A$ is in row echelon form if:

Row Echelon Form: Definition 1.5

Leading Entry is 1: $\forall i \in \mathbb{N}_{\le m} \; \exists j \in \mathbb{N}_{\le n} \mid a_{ij} = 1 \land \bigwedge_{k=i}^{m} a_{kj}=0 \implies \bigwedge_{k=1}^{j} a_{kj} = 0$

Leading Entry is the Only Non-Zero Entry in its Column: $\forall i \in \mathbb{N}_{\le m} \; \exists j \in \mathbb{N}_{\le n} \mid a_{ij} = 1 \land \bigwedge_{k=i}^{m} a_{kj}=0 \implies \forall k \in \mathbb{N}_{\le m} \mid k \neq i \implies a_{kj} = 0$

  • $\begingroup$ What is $\bigwedge$ here? $\endgroup$
    – pancini
    Nov 20 at 19:19
  • 5
    $\begingroup$ Please do not use images to convey information not otherwise present in your post. See here for why. $\endgroup$ Nov 20 at 19:28
  • $\begingroup$ @pancini: The "and" logical connective. $\endgroup$ Nov 20 at 19:28
  • 1
    $\begingroup$ You might find it a useful exercise to write things out in symbolic formal logic like this, but I think most people find it easier to work with natural-language statements (as long as they can be made clear and precise). Mathematical writing is communication with other humans, not computer programming. $\endgroup$
    – Karl
    Nov 22 at 16:37
  • 1
    $\begingroup$ @Karl I am trying to think of proofs in a more formal way, I guess this approach might help a little since it makes every definition more clear and precise. However, even if it didn't help, it would've been a great exercise to deepen one's understanding. $\endgroup$ Nov 23 at 17:57


You must log in to answer this question.

Browse other questions tagged .