star_star
theorem star_star : ∀ {R : Type u} [inst : InvolutiveStar R] (r : R), star (star r) = r
This theorem, `star_star`, states that for any given type `R` with an `InvolutiveStar` instance (which is a type class representing types with an involution operation denoted by `star`), applying the `star` operation twice on an element `r` of type `R` yields the original element `r`. In mathematical terms, this is saying that the `star` operation is its own inverse. In the context of algebraic structures, this would typically be seen in structures where an operation is self-inverse, such as taking a complex conjugate twice in complex numbers.
More concisely: For any type `R` with an `InvolutiveStar` instance, the operation `star` is idempotent, i.e., `star (star r) = r` for all `r` in `R`.
|
TrivialStar.star_trivial
theorem TrivialStar.star_trivial : ∀ {R : Type u} [inst : Star R] [self : TrivialStar R] (r : R), star r = r
This theorem states that for any type `R` that is equipped with a `Star` operation and satisfies the `TrivialStar` property, the `Star` operation on any element `r` of `R` returns the element itself. In other words, for any `r` in `R`, `star r = r`. The `Star` operation is assumed to be trivial (i.e., it does not change the element) for all elements of `R`.
More concisely: For any type `R` with a trivial `Star` operation satisfying `TrivialStar` property, `star r = r` for all `r` in `R`.
|
Mathlib.Algebra.Star.Basic._auxLemma.6
theorem Mathlib.Algebra.Star.Basic._auxLemma.6 :
∀ {R : Type u} [inst : AddMonoid R] [inst_1 : StarAddMonoid R] {x : R}, (star x = 0) = (x = 0)
This theorem, located in the `Mathlib.Algebra.Star.Basic` module under the name `_auxLemma.6`, states that for any type `R` that has an `AddMonoid` and `StarAddMonoid` structure, and for any element `x` of `R`, the star of `x` is zero if and only if `x` is zero. In other words, the `star` operation, which is part of the `StarAddMonoid` structure, preserves the zero element of the `AddMonoid`.
More concisely: For any type `R` with an `AddMonoid` and `StarAddMonoid` structure, the star of any element `x` in `R` is zero if and only if `x` is zero.
|
conj_trivial
theorem conj_trivial :
∀ {R : Type u} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TrivialStar R] (a : R),
(starRingEnd R) a = a
This theorem states that for any type `R` that is a commutative semiring and also a star ring with the trivial star operation, if `a` is an element of `R`, then the star of `a` is equal to `a` itself. More formally, this theorem says that for any `a` in `R`, `starRingEnd R a = a`. The `starRingEnd R` function applies the star operation to `a`, and the `TrivialStar` class asserts that the star operation is the identity. This theorem is therefore a specification of the behavior of the star operation in a commutative semiring that is also a star ring with trivial star operation.
More concisely: In a commutative semiring `R` with trivial star operation, the star of any element `a` in `R` equals `a` itself.
|
InvolutiveStar.star_involutive
theorem InvolutiveStar.star_involutive : ∀ {R : Type u} [self : InvolutiveStar R], Function.Involutive star
The theorem `InvolutiveStar.star_involutive` states that for any type `R` that has an instance of the `InvolutiveStar` structure, the `star` function is involutive. In other words, applying the `star` function twice to any element of `R` will return the original element, i.e., for all `x` in `R`, `star (star x) = x`. This property is a general feature in mathematics for operations called "involutions", which include operations like taking the reciprocal or the negative of a number, or the transpose of a matrix.
More concisely: For any type `R` equipped with an `InvolutiveStar` structure, the `star` operation is an involution, i.e., `star (star x) = x` for all `x` in `R`.
|
star_id_of_comm
theorem star_id_of_comm : ∀ {R : Type u_1} [inst : CommSemiring R] {x : R}, star x = x
This theorem states that for any type `R` that is a commutative semiring and any element `x` of `R`, the 'star' operation on `x` is equal to `x` itself. Notably, even though a proof is not provided here, this result can be derived automatically by the `simp` function owing to the reducibility of the `starMulOfComm` function.
More concisely: For any commutative semiring `R` and its element `x`, the `star` operation on `x` equals `x` (i.e., `star x = x`).
|
star_neg
theorem star_neg : ∀ {R : Type u} [inst : AddGroup R] [inst_1 : StarAddMonoid R] (r : R), star (-r) = -star r := by
sorry
This theorem, named `star_neg`, states that for any type `R` that forms an add group and a star add monoid, the star operation applied to the negation of an element `r` of `R` equals the negation of the star of `r`. In more familiar terms, this corresponds to the mathematical property that the star operation and negation commute in some sort of way. In the language of algebra, if you have a certain structure (like a group with an additional operation, here denoted as `star`), the way negation and the `star` operation interact is specified by this theorem. The star of the negative of `r` is the same as the negative of the star of `r`.
More concisely: For any add group and star add monoid `R`, the star of the additive negation of an element `r` equals the additive negation of the star of `r`: `-(star r) = star (-r)`.
|
star_one
theorem star_one : ∀ (R : Type u) [inst : MulOneClass R] [inst_1 : StarMul R], star 1 = 1
This theorem states that for any type `R` that has a multiplication and a unit element (as specified by the `MulOneClass` typeclass) and also supports the star multiplication operation (as specified by the `StarMul` typeclass), the star of the unit element `1` is equal to `1`. In mathematical terms, it says that the star operation is a unital operation on `R`, i.e., the identity element remains unchanged under the star operation.
More concisely: For any type `R` with multiplication and a unit element, and having a star multiplication operation, the star of the unit element is equal to the unit element (i.e., 1 * is = 1).
|
star_sub
theorem star_sub :
∀ {R : Type u} [inst : AddGroup R] [inst_1 : StarAddMonoid R] (r s : R), star (r - s) = star r - star s
This theorem, `star_sub`, states that for any type `R` where `R` is an additive group and a star-additive monoid, for any elements `r` and `s` of `R`, the star of the difference between `r` and `s` is equal to the difference between the star of `r` and the star of `s`. In mathematical terminology, it says that the star operation, a kind of unary operation, distributes over subtraction in this specific algebraic structure.
More concisely: For any additive group and star-additive monoid `R`, the star operation distributes over subtraction, that is, `*(r - s) = *r - *s` for all `r, s ∈ R`.
|
StarModule.star_smul
theorem StarModule.star_smul :
∀ {R : Type u} {A : Type v} [inst : Star R] [inst_1 : Star A] [inst_2 : SMul R A] [self : StarModule R A] (r : R)
(a : A), star (r • a) = star r • star a
This theorem, `StarModule.star_smul`, states that the `star` operation (often used to denote complex conjugation or other "star" operations in mathematics) commutes with scalar multiplication in the context of star modules. Given a ring `R`, a type `A`, a scalar `r` of type `R`, and an element `a` of type `A`, the theorem shows that applying the `star` operation to the result of scalar multiplication of `r` and `a` is the same as the scalar multiplication of the `star` of `r` and the `star` of `a`.
More concisely: For any ring R, star module A, scalar r in R, and element a in A, the application of the star operation to the scalar multiplication of r and a is equal to the scalar multiplication of the star of r and the star of a. In other words, (r \* a)^\* = r^\* \* a^\*.
|
star_injective
theorem star_injective : ∀ {R : Type u} [inst : InvolutiveStar R], Function.Injective star
The theorem `star_injective` states that for every type `R` equipped with an instance of the `InvolutiveStar` structure, the `star` function (which is part of the `InvolutiveStar` structure) is injective. In other words, for any two elements `a₁` and `a₂` of `R`, if `star a₁` equals `star a₂`, then `a₁` must equal `a₂`. This injectivity property holds regardless of the specific type `R` or the specifics of the `InvolutiveStar` instance.
More concisely: For every type `R` endowed with an `InvolutiveStar` structure, the `star` function is a injective function on `R`.
|
SemiconjBy.star_star_star
theorem SemiconjBy.star_star_star :
∀ {R : Type u} [inst : Mul R] [inst_1 : StarMul R] {x y z : R},
SemiconjBy x y z → SemiconjBy (star x) (star z) (star y)
This theorem, `SemiconjBy.star_star_star`, states that for any type `R` with multiplication and star multiplication operations, if `x` is semiconjugate to `y` by `z` (meaning `z * x = y * z`), then the star of `x` is semiconjugate to the star of `y` by the star of `z` (meaning `star(z) * star(x) = star(y) * star(z)`). In mathematical terms, if `zx = yz`, then `z* * x* = y* * z*`. The star operation is a generalization of complex conjugation.
More concisely: If `x` is semiconjugate to `y` by `z`, then the star of `x` is semiconjugate to the star of `y` by the star of `z` (i.e., `z * * x = y * * z`).
|
star_pow
theorem star_pow : ∀ {R : Type u} [inst : Monoid R] [inst_1 : StarMul R] (x : R) (n : ℕ), star (x ^ n) = star x ^ n
This theorem, `star_pow`, states that for any type `R` that has a monoid structure and a star-multiplication structure, given any element `x` of `R` and any natural number `n`, the star of `x` raised to the power `n` is equal to the star of `x` raised to the power `n`. In mathematical terms, if `*` denotes the star operation and `^` denotes exponentiation, this states that `(x^n)* = (x*)^n` for all `x` in `R` and `n` in ℕ. This is a property relating the star operation and exponentiation in any star-multiplicative monoid.
More concisely: For any star-multiplicative monoid `(R, *, *)`, and for all `x ∈ R` and `n ∈ ℕ`, `(x^n)^* = (x*)^n`.
|
star_div
theorem star_div : ∀ {R : Type u} [inst : CommGroup R] [inst_1 : StarMul R] (x y : R), star (x / y) = star x / star y
This theorem states that, in the context of a type `R` that forms a commutative group under multiplication and also supports a `star` operation, the `star` operation preserves the division operation. Formally, for any elements `x` and `y` of `R`, applying the `star` operation to the result of dividing `x` by `y` yields the same result as dividing the `star` of `x` by the `star` of `y`.
More concisely: If `R` is a commutative group with multiplication and has a `star` operation such that `x * (y \*\* -1) = (x \*\* -1) * star(y)` for all `x, y ∈ R`, then `star(x / y) = star(x) / star(y)`.
|
StarRing.star_add
theorem StarRing.star_add :
∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] [self : StarRing R] (r s : R), star (r + s) = star r + star s
This theorem, `star_add`, states that for any type `R` which is a `NonUnitalNonAssocSemiring` (a kind of mathematical structure similar to a ring but without the requirement for a multiplicative identity or an associative multiplication) and also a `StarRing` (a ring with a * operation), the `star` operation commutes with addition. More formally, for any elements `r` and `s` of `R`, the `star` of the sum of `r` and `s` is equal to the sum of the `star` of `r` and the `star` of `s`. In mathematical notation, this would be expressed as *(`r` + `s`) = *`r` + *`s`.
More concisely: For any `NonUnitalNonAssocSemiring` and `StarRing` `R`, `*` (star) operation commutes with addition: `* (r + s) = * r + * s`.
|
star_zero
theorem star_zero : ∀ (R : Type u) [inst : AddMonoid R] [inst_1 : StarAddMonoid R], star 0 = 0
This theorem states that for any type `R` which has both an additive monoid structure and a 'star' additive monoid structure, if we apply the 'star' operation to the zero element of the additive monoid, we will get the zero element back. In mathematical terms, if `R` is an additive monoid and a star additive monoid, then the star of zero in `R` is equal to zero.
More concisely: For any additive monoid and star additive monoid `R`, the star of its additive identity is equal to the additive identity itself.
|
StarAddMonoid.star_add
theorem StarAddMonoid.star_add :
∀ {R : Type u} [inst : AddMonoid R] [self : StarAddMonoid R] (r s : R), star (r + s) = star r + star s
This theorem, `StarAddMonoid.star_add`, states that in any star-additive monoid `R`, the `star` operation commutes with addition. More formally, for any elements `r` and `s` of `R`, the star of the sum of `r` and `s` is equal to the sum of the star of `r` and the star of `s`. A star-additive monoid is a structure where `star` is an additional operation that satisfies certain conditions, and this theorem states one of these conditions.
More concisely: In a star-additive monoid, the star operation commutes with addition, that is, for all elements `r` and `s`, `(r + s)^* = r^* + s^*`.
|
starRingEnd_self_apply
theorem starRingEnd_self_apply :
∀ {R : Type u} [inst : CommSemiring R] [inst_1 : StarRing R] (x : R), (starRingEnd R) ((starRingEnd R) x) = x := by
sorry
The theorem `starRingEnd_self_apply` states that for any type `R` that is a commutative semiring with a star operation (denoted as `StarRing R`), applying the `starRingEnd` operation twice to any element `x` of `R` returns the original element `x`. In other words, the `starRingEnd` operation is its own inverse.
More concisely: For any commutative semiring `R` with a star operation, `StarRing R x = x` for all `x` in `R`.
|
Commute.star_star
theorem Commute.star_star :
∀ {R : Type u} [inst : Mul R] [inst_1 : StarMul R] {x y : R}, Commute x y → Commute (star x) (star y)
This theorem, which can be referred to as an alias of the reverse direction of `commute_star_star`, states that for any type `R` that supports multiplication (`Mul R`) and star multiplication (`StarMul R`), if two elements `x` and `y` of `R` commute, then the star of `x` and the star of `y` also commute. Here, two elements are said to commute if the order of their multiplication does not matter (i.e., `a * b = b * a`), and "star" refers to an operation defined in the context of `StarMul R`.
More concisely: If `x` and `y` in type `R` with multiplication and star multiplication commute (i.e., `x * y = y * x`), then their star counterparts also commute (i.e., `*(x :* R) * *(y :* R) = *(y :* R) * *(x :* R)`).
|
star_bit0
theorem star_bit0 :
∀ {R : Type u} [inst : AddMonoid R] [inst_1 : StarAddMonoid R] (r : R), star (bit0 r) = bit0 (star r)
This theorem, named `star_bit0`, states that for all objects `r` of some type `R`, where `R` is equipped with an addition operation forming an additive monoid, and also equipped with a `star` operation forming a star-additive monoid, the `star` of the bit doubling operation applied to `r` is equal to the bit doubling operation applied to the `star` of `r`. In other words, in the context of these algebraic structures, the `star` operation and the bit doubling operation commute with each other.
More concisely: For all additive monoid `R` with a star operation making it a star-additive monoid, the star of the bit doubling operation applied to an element `r` equals the bit doubling operation applied to the star of `r`: `(*(2 & r) = 2 & *(r))`.
|
Mathlib.Algebra.Star.Basic._auxLemma.1
theorem Mathlib.Algebra.Star.Basic._auxLemma.1 :
∀ {R : Type u} [inst : InvolutiveStar R] {x y : R}, (star x = star y) = (x = y)
This theorem, labeled as `Mathlib.Algebra.Star.Basic._auxLemma.1`, states that for any type `R` equipped with an operation `star` that is involutive (meaning applying `star` twice yields the original element), and any two elements `x` and `y` of type `R`, the proposition that the `star` of `x` equals the `star` of `y` is equivalent to the proposition that `x` equals `y`. In simpler words, if the `star` operation applied to `x` and `y` gives the same result, then `x` and `y` are themselves equal.
More concisely: For any type `R` and involutive operation `star` on `R`, if `x` and `y` in `R` satisfy `star x = star y`, then `x = y`.
|
star_mul'
theorem star_mul' :
∀ {R : Type u} [inst : CommSemigroup R] [inst_1 : StarMul R] (x y : R), star (x * y) = star x * star y
This theorem states that in a commutative ring with a star operation, the star of the product of two elements is equal to the product of the stars of those elements. In more mathematical terms, given a commutative semigroup `R` with a star operation `star`, for any two elements `x` and `y` in `R`, the operation `star (x * y)` is equivalent to `star x * star y`. This essentially means that the order of operations doesn't matter - you can either multiply the two elements first and then apply the star operation, or you can apply the star operation to each element first and then multiply the results. This property is used to make `simp` prefer leaving the order unchanged in Lean's simplification process.
More concisely: In a commutative semigroup equipped with a star operation, the star of the product of any two elements equals the product of their stars.
|
IsUnit.star
theorem IsUnit.star : ∀ {R : Type u} [inst : Monoid R] [inst_1 : StarMul R] {a : R}, IsUnit a → IsUnit (star a) := by
sorry
The theorem `IsUnit.star` states that for any type `R` that is a `Monoid` and also has a `StarMul` structure, if an element `a` of `R` is a unit (i.e., it has a two-sided inverse), then its star (obtained by applying the `star` operation from the `StarMul` structure) is also a unit. In other words, the `star` operation preserves the property of being a unit in the monoid.
More concisely: If `R` is a monoid with a `StarMul` structure and `a` is a unit in `R`, then the star of `a` (obtained from the `star` operation in `StarMul`) is also a unit in `R`.
|
StarHomClass.map_star
theorem StarHomClass.map_star :
∀ {F : Type u_1} {R : outParam (Type u_2)} {S : outParam (Type u_3)} [inst : Star R] [inst_1 : Star S]
[inst_2 : FunLike F R S] [self : StarHomClass F R S] (f : F) (r : R), f (star r) = star (f r)
The theorem `StarHomClass.map_star` states that for all types `F`, `R`, and `S`, given that `R` and `S` have a star operation defined on them (demonstrated by the instances `[inst : Star R]` and `[inst_1 : Star S]`), and function-type `F` can be injectively coerced into a function from `R` to `S` (indicated by `[inst_2 : FunLike F R S]`), if `F` also carries a structure of a star homomorphism (shown by `[self : StarHomClass F R S]`), then for any function `f` of type `F` and any element `r` of type `R`, applying `f` to the star of `r` (i.e., `f (star r)`) is equivalent to taking the star of `f(r)` (i.e., `star (f r)`), hence preserving the star operation under the map `f`.
More concisely: If `F` is a star homomorphism from `R` to `S` with `R` and `S` being star operations, then applying `F` to the star of an element in `R` equals taking the star of the image of that element under `F`.
|
starRingEnd_apply
theorem starRingEnd_apply :
∀ {R : Type u} [inst : CommSemiring R] [inst_1 : StarRing R] (x : R), (starRingEnd R) x = star x
This theorem, `starRingEnd_apply`, states that for any element `x` of a type `R` that has both a commutative semiring structure and a star ring structure, the application of the `starRingEnd` function to `x` yields the same result as the application of the `star` function to `x`. This isn't used as a simplification lemma as it's generally more beneficial to keep `starRingEnd` bundled. For instance, in the case of complex conjugation, we wouldn't want Lean to automatically simplify `conj x` to `star x`, as most theorems are about `conj x`.
More concisely: For any element `x` in a commutative semiring with a star ring structure, `starRingEnd x` equals `star x`.
|
star_inv'
theorem star_inv' : ∀ {R : Type u} [inst : DivisionSemiring R] [inst_1 : StarRing R] (x : R), star x⁻¹ = (star x)⁻¹
This theorem, called `star_inv'`, is applicable to any type `R` that is a division semiring and a star ring. The theorem states that for any element `x` of type `R`, the star operation applied to the inverse of `x` is equivalent to the inverse of the star of `x`. Formally, for all `x` in `R`, `star x⁻¹ = (star x)⁻¹`. The star operation here typically represents the complex conjugate or some form of involution in a star ring.
More concisely: For any element `x` in a division semiring and star ring `R`, the star of the multiplicative inverse of `x` equals the multiplicative inverse of the star of `x`: `star (x^(-1)) = (star x)^(-1)`.
|
StarMul.star_mul
theorem StarMul.star_mul : ∀ {R : Type u} [inst : Mul R] [self : StarMul R] (r s : R), star (r * s) = star s * star r
This theorem states that the `star` operation skew-distributes over multiplication in any type `R` that supports the `Mul` (multiplication) and `StarMul` operations. More specifically, for any elements `r` and `s` of the type `R`, the `star` of the product of `r` and `s` is equal to the product of the `star` of `s` and the `star` of `r`. Please note that the order of multiplication is reversed.
More concisely: For any type `R` with operations `Star`, `Mul` such that `R` is a commutative ring, `star` skew-distributes over multiplication: `star (r * s) = star s * star r`.
|
star_div'
theorem star_div' :
∀ {R : Type u} [inst : Semifield R] [inst_1 : StarRing R] (x y : R), star (x / y) = star x / star y
This theorem states that for any type `R` that is both a semifield and a star ring, the `star` operation preserves the operation of division. In other words, for any elements `x` and `y` of `R`, the `star` of the quotient of `x` and `y` is equal to the quotient of the `star` of `x` and the `star` of `y`. Here, a semifield is a field that may not have an additive identity and a StarRing is a structure on a ring that implements an involution (an operation that is its own inverse).
More concisely: For any semifield and star ring `R`, the `star` operation preserves division, that is, `*(x / y) = (*(x) / *(y))` for all `x, y ∈ R`.
|
StarMemClass.star_mem
theorem StarMemClass.star_mem :
∀ {S : Type u_1} {R : Type u_2} [inst : Star R] [inst_1 : SetLike S R] [self : StarMemClass S R] {s : S} {r : R},
r ∈ s → star r ∈ s
This theorem is about the concept of closure under the "star" operation in the context of set-like structures. It states that for any types `S` and `R`, given the `Star` instance for `R` and the `SetLike` and `StarMemClass` instances for `S` and `R`, if a member `r` belongs to a set `s`, then the "star" of `r` (denoted as `star r`) also belongs to the same set `s`. This is essentially saying that the set `s` is closed under the "star" operation.
More concisely: If `S` is a set-like structure with `SetLike` and `StarMemClass` instances, and `R` has a `Star` instance, then `star r ∈ s` given `r ∈ s`.
|
Complex.conj_conj
theorem Complex.conj_conj :
∀ {R : Type u} [inst : CommSemiring R] [inst_1 : StarRing R] (x : R), (starRingEnd R) ((starRingEnd R) x) = x := by
sorry
This theorem, named `Complex.conj_conj`, states that for any type `R` that is a commutative semiring and a star ring, applying the `starRingEnd` function twice on any element `x` of type `R` will return the original element `x`. Essentially, this means that the `starRingEnd` function is involutive in this context, i.e., it is its own inverse when applied twice.
More concisely: For any commutative semiring and star ring `R`, the involution `starRingEnd : R → R` satisfies `starRingEnd (starRingEnd x) = x` for all `x : R`.
|