JetBrains / arend-lib

Apache License 2.0
79 stars 23 forks source link

Prove a lemma about homogeneous decomposition #57

Closed valis closed 1 year ago

valis commented 1 year ago

Let R be a graded ring. Suppose we have a homogeneous element x, which is equal to \sum_{1 <= i <= n} a_i b_i, where a_i are homogeneous. Then we can decompose b_i into homogeneous elements b_i^1 + ... + b_i^{k_i}. By uniqueness of decomposition of x, there is at most one b_i^{j_i} such that a_i * b_i^{ji} is non-zero. It follows that x is equal to \sum{1 <= i <= n} a_i b'_i, where b'_i are homogeneous. This goal should prove this equality.

ice1000 commented 1 year ago

Let $R$ be a graded ring. Suppose we have a homogeneous element x, which is equal to $\sum_{1 \leq i \leq n} a_i b_i$, where $a_i$ are homogeneous. Then we can decompose $b_i$ into homogeneous elements $b_i^1 + ... + b_i^{k_i}$. By uniqueness of decomposition of $x$, there is at most one $b_i^{j_i}$ such that $a_i \times b_i^{ji}$ is non-zero. It follows that $x$ is equal to $\sum{1 \leq i \leq n} a_i b'_i$, where $b'_i$ are homogeneous. This goal should prove this equality.

valis commented 1 year ago

@ice1000 How did you do that?)

ice1000 commented 1 year ago

@ice1000 How did you do that?)

https://docs.github.com/en/get-started/writing-on-github/working-with-advanced-formatting/writing-mathematical-expressions