# Validity of the Definition of Row Echelon Form

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$$

• What is $\bigwedge$ here? Commented Nov 20, 2023 at 19:19
• Please do not use images to convey information not otherwise present in your post. See here for why. Commented Nov 20, 2023 at 19:28
• @pancini: The "and" logical connective. Commented Nov 20, 2023 at 19:28
• 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.
– Karl
Commented Nov 22, 2023 at 16:37
• @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. Commented Nov 23, 2023 at 17:57