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$
