uniq_inv_of_isField
theorem uniq_inv_of_isField : ∀ (R : Type u) [inst : Ring R], IsField R → ∀ (x : R), x ≠ 0 → ∃! y, x * y = 1
This theorem states that for any given field, and for any non-zero element of that field, there exists a unique inverse. More specifically, for any type `R` that has structure of a Ring, if `R` also satisfies conditions of a field (`IsField R`), then for every non-zero element `x` of `R`, there exists exactly one element `y` in `R` such that the product of `x` and `y` equals the multiplicative identity `1`. This theorem can be useful because the `IsField` structure does not inherently include an inverse function, so a lemma providing the existence and uniqueness of inverses can be beneficial.
More concisely: For any field `R`, every non-zero element `x` in `R` has a unique multiplicative inverse.
|
Semifield.toIsField
theorem Semifield.toIsField : ∀ (R : Type u) [inst : Semifield R], IsField R
This theorem states that for any type `R` that has a `Semifield` structure, it can be seen as having an `IsField` structure. In mathematical terms, it suggests that any semi-field can be viewed as a field, which means all the properties of a field hold true for a semi-field.
More concisely: A semi-field is a field with the additional requirement that every non-zero element has an additive multiplicative inverse. Thus, every semi-field is a field.
|
IsField.mul_comm
theorem IsField.mul_comm : ∀ {R : Type u} [inst : Semiring R], IsField R → ∀ (x y : R), x * y = y * x
This theorem states that for any type `R` that is a semiring and a field, multiplication is commutative. In other words, for all elements `x` and `y` of `R`, the product of `x` and `y` is the same as the product of `y` and `x`. In mathematical terms, this can be written as: for all `x`, `y` in `R`, `x * y = y * x`.
More concisely: For any semiring and field `R`, the multiplication operation is commutative. In other words, for all `x, y` in `R`, `x * y = y * x`.
|
Field.toIsField
theorem Field.toIsField : ∀ (R : Type u) [inst : Field R], IsField R
This theorem states that for any type 'R' which is a 'Field', 'R' is also an 'IsField'. In other words, the structure 'Field' implies the structure 'IsField'. This is a structural transfer theorem, converting or viewing a field as an 'IsField' in the context of abstract algebra.
More concisely: For any field 'R', 'R' has the structure of an IsField.
|
IsField.mul_inv_cancel
theorem IsField.mul_inv_cancel : ∀ {R : Type u} [inst : Semiring R], IsField R → ∀ {a : R}, a ≠ 0 → ∃ b, a * b = 1 := by
sorry
This theorem asserts that if we have a non-zero element in a field, then there exists a multiplicative inverse for that element. More formally, for any type `R` that has a semiring structure, if `R` is a field and `a` is an element of `R` that is not equal to zero, then there exists another element `b` in `R` such that the product of `a` and `b` equals 1, which is the multiplicative identity in the field `R`.
More concisely: In a field, every non-zero element has a multiplicative inverse.
|
IsField.exists_pair_ne
theorem IsField.exists_pair_ne : ∀ {R : Type u} [inst : Semiring R], IsField R → ∃ x y, x ≠ y
This theorem states that for any semiring `R`, if `R` is a field, then it must have at least two distinct elements. In other words, there exist two elements `x` and `y` in `R` such that `x` is not equal to `y`.
More concisely: If `R` is a field in Lean 4, then `R` has at least two distinct elements.
|