RingEquiv.injective
theorem RingEquiv.injective :
∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S),
Function.Injective ⇑e
The theorem `RingEquiv.injective` states that for any two types `R` and `S` which have multiplication and addition operations defined, any ring equivalence `e : R ≃+* S` is injective. In other words, if `e` maps two elements of `R` to the same element in `S`, then those two elements must be the same. This is a property of ring isomorphisms, which are bijective mappings that preserve both addition and multiplication.
More concisely: If `e : R ≃+* S` is a ring equivalence between types `R` and `S`, then `e` is an injection (i.e., for all `a, b ∈ R`, if `e(a) = e(b)`, then `a = b`).
|
MulEquiv.isDomain
theorem MulEquiv.isDomain :
∀ {A : Type u_7} (B : Type u_8) [inst : Semiring A] [inst_1 : Semiring B] [inst_2 : IsDomain B],
A ≃* B → IsDomain A
This theorem states that if two structures (specifically, two rings) of type A and B are isomorphic, and if the type B is a domain (which means it is a non-zero commutative ring in which the product of any two non-zero elements is also non-zero), then type A is also a domain. This theorem is applicable for any types A and B where A is a semiring and B is a semiring and a domain. The isomorphism between A and B is denoted as `A ≃* B` . This is a key result in ring theory, showing the preservation of the domain property under ring isomorphisms.
More concisely: If two semiring structures are isomorphic and one is a domain, then the other is also a domain.
|
RingEquiv.toAddMonoidMom_commutes
theorem RingEquiv.toAddMonoidMom_commutes :
∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R ≃+* S),
(↑f).toAddMonoidHom = (↑f).toAddMonoidHom
This theorem states that for any two types `R` and `S`, which are non-associative semirings, the two paths that coercion can take to an `AddMonoidHom` are equivalent. In other words, for any ring equivalence `f` from `R` to `S`, the additive monoid homomorphism obtained by coercing `f` is the same regardless of the path taken during coercion. The theorem is applicable for any ring homomorphism, without exceptions.
More concisely: For any non-associative semirings R and S, and any ring equivalence f from R to S, the additive monoid homomorphisms obtained by coercing f are equal.
|
RingEquiv.ext
theorem RingEquiv.ext :
∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] {f g : R ≃+* S},
(∀ (x : R), f x = g x) → f = g
This theorem states that for any two types `R` and `S`, both having multiplication and addition operations, and for any two ring isomorphisms `f` and `g` from `R` to `S`, if these isomorphisms act identically on all elements of `R` (that is, for each element `x` in `R`, `f(x)` is equal to `g(x)`), then `f` and `g` are actually the same isomorphism. A ring isomorphism here is a bijection that preserves the ring operations, namely addition and multiplication.
More concisely: If two ring isomorphisms between types with multiplication and addition operations agree on all elements, then they are equal.
|
RingEquiv.toEquiv_commutes
theorem RingEquiv.toEquiv_commutes :
∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R ≃+* S),
(↑f).toEquiv = (↑f).toEquiv
This theorem states that for any two types `R` and `S` that are instances of the `NonAssocSemiring` class, and for any ring isomorphism `f` from `R` to `S`, the two coercion paths that `f` can take to an `Equiv` (a type representing reversible functions) are equivalent. Essentially, it's asserting that the process of converting a ring isomorphism into an equivalence relation is unambiguous and consistent, regardless of the specific coercion path followed.
More concisely: Given two types `R` and `S` instantiating `NonAssocSemiring`, and a ring isomorphism `f` from `R` to `S`, the coercions `f : R ⊎ S →* R` and `f : R ⊎ S →* S` define equivalent equivalence relations on `R ⊎ S`.
|
RingEquiv.map_one
theorem RingEquiv.map_one :
∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R ≃+* S), f 1 = 1
This theorem states that for any ring isomorphism `f` between two non-associative semirings `R` and `S`, the image of the multiplicative identity (1) under `f` is also the multiplicative identity (1) in `S`. In other words, a ring isomorphism preserves the multiplicative identity.
More concisely: For any ring isomorphisms f between semirings R and S, f(1) = 1 in S.
|
RingEquiv.map_add
theorem RingEquiv.map_add :
∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S)
(x y : R), e (x + y) = e x + e y
This theorem, `RingEquiv.map_add`, states that for any two types `R` and `S` that both have multiplication (`Mul`) and addition (`Add`) structures, any ring isomorphism (denoted by `≃+*`) from `R` to `S` preserves the addition operation. More specifically, if `x` and `y` are elements of `R`, then applying the isomorphism to the sum of `x` and `y` (`x + y`) is the same as applying the isomorphism to `x` and `y` separately and then adding the results.
More concisely: Given ring isomorphisms `f : R ≃+* S`, `x, y ∈ R`, we have `f(x + y) = f(x) + f(y)`.
|
RingEquiv.map_add'
theorem RingEquiv.map_add' :
∀ {R : Type u_7} {S : Type u_8} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (self : R ≃+* S)
(x y : R), self.toFun (x + y) = self.toFun x + self.toFun y
This theorem states that for any types `R` and `S` equipped with both multiplication and addition operations, and for any ring isomorphism `self` mapping from `R` to `S`, the function `self` preserves addition. More explicitly, given any elements `x` and `y` of `R`, the result of applying `self` to the sum of `x` and `y` equals the sum of the results of applying `self` to `x` and `y` individually. This property is crucial in maintaining the structure of a ring during the isomorphism.
More concisely: Given any ring isomorphisms `f : R → S` between types `R` and `S` equipped with multiplication and addition operations, `f (x + y) = f x + f y` for all `x, y ∈ R`.
|
RingEquivClass.map_add
theorem RingEquivClass.map_add :
∀ {F : Type u_7} {R : Type u_8} {S : Type u_9} [inst : Mul R] [inst_1 : Add R] [inst_2 : Mul S] [inst_3 : Add S]
[inst_4 : EquivLike F R S] [self : RingEquivClass F R S] (f : F) (a b : R), f (a + b) = f a + f b
This theorem, `RingEquivClass.map_add`, states that for any types `F`, `R`, and `S`, where `R` and `S` have both multiplication and addition operations, and `F` is an equivalence relation between `R` and `S`, if there exists a ring isomorphism between `R` and `S`, then this isomorphism preserves the additive structure. In other words, the isomorphism of an addition of two elements in `R` is the same as the sum of the isomorphisms of the two elements. This holds for all elements `a` and `b` in `R` and any function `f` of type `F`.
More concisely: If `F` is an equivalence relation on rings `R` and `S` with a ring isomorphism `f : R ≅ S`, then `f(a +\_R b) = f(a) +\_S f(b)` for all `a, b ∈ R`.
|
RingEquiv.map_mul'
theorem RingEquiv.map_mul' :
∀ {R : Type u_7} {S : Type u_8} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (self : R ≃+* S)
(x y : R), self.toFun (x * y) = self.toFun x * self.toFun y
This theorem states that a ring homomorphism (denoted by `self`) preserves multiplication. More specifically, for all types `R` and `S` that have multiplication and addition structures, if we have a ring equivalence from `R` to `S`, for any two elements `x` and `y` of `R`, the result of applying the ring equivalence to the product of `x` and `y` (`x * y`) is the same as the product of the results of applying the ring equivalence to `x` and `y` individually. In mathematical terms, this can be written as `self(x*y) = self(x) * self(y)`, which is a fundamental property of ring homomorphisms.
More concisely: A ring homomorphism maps the product of two elements to the product of their images: `self(x * y) = self(x) * self(y)`.
|
RingEquiv.surjective
theorem RingEquiv.surjective :
∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S),
Function.Surjective ⇑e
The theorem `RingEquiv.surjective` states that for any two types `R` and `S` with multiplication (`Mul`) and addition (`Add`) operations, if there exists a ring equivalence `e` between `R` and `S`, then `e` is a surjective function. In other words, for every element in `S`, there is an element in `R` such that applying `e` to this element of `R` gives the original element of `S`.
More concisely: If `e: R ≃ R'` is a ring equivalence between rings `(R, +, *)` and `(R', +', *)`, then `e` is a surjective function.
|
RingEquiv.map_mul
theorem RingEquiv.map_mul :
∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S)
(x y : R), e (x * y) = e x * e y
This theorem states that a ring isomorphism preserves multiplication. In other words, if you have a ring isomorphism `e` between two rings `R` and `S`, and two elements `x` and `y` from the ring `R`, then the image of the product `x * y` under the isomorphism `e` is the same as the product of the images `e x` and `e y`. This is a fundamental property of ring isomorphisms.
More concisely: If `e` is a ring isomorphism between rings `R` and `S`, then for all `x, y ∈ R`, `e(x * y) = e(x) * e(y)`.
|
RingEquiv.map_zero
theorem RingEquiv.map_zero :
∀ {R : Type u_4} {S : Type u_5} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
(f : R ≃+* S), f 0 = 0
This theorem states that for any ring isomorphism `f`, where `f` is a map between two types `R` and `S` that are non-unital, non-associative semirings, the image of `0` from `R` under `f` is `0` in `S`. In other words, a ring isomorphism preserves the zero element: it maps zero to zero.
More concisely: For any non-unital, non-associative semiring isomorphism `f` between types `R` and `S`, `f(0_R) = 0_S`.
|
RingEquiv.toNonUnitalRingHom_commutes
theorem RingEquiv.toNonUnitalRingHom_commutes :
∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R ≃+* S), ↑↑f = ↑f
This theorem states that for any two types `R` and `S` that are non-associated semirings, any given ring equivalence `f` between `R` and `S` can be treated equivalently whether it is first coerced to a `NonUnitalRingEquiv` and then to a `NonUnitalRingHom`, or directly coerced to a `NonUnitalRingHom`. This is expressed by the equality `↑↑f = ↑f`, where `↑↑f` and `↑f` denote the two different coercion paths.
More concisely: For any non-associated semirings R and S and any ring equivalence f between them, the coercion of f to a NonUnitalRingEquiv and then to a NonUnitalRingHom is equal to the direct coercion of f to a NonUnitalRingHom: ↑↑f = ↑f.
|
RingEquiv.symm_comp
theorem RingEquiv.symm_comp :
∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (e : R ≃+* S),
(↑e.symm).comp ↑e = RingHom.id R
This theorem states that for any non-associative semiring `R` and `S`, given a ring isomorphism `e` from `R` to `S`, the composition of the ring homomorphism of `e` and its inverse is equal to the identity ring homomorphism on `R`. In other words, applying the isomorphism and then its inverse leaves any element in the semiring `R` unchanged, which is a characteristic property of isomorphisms in mathematics.
More concisely: For any non-associative semiring isomorphism `e` from `R` to `S`, `e ∘ eᵀ = id_R`, where `id_R` is the identity ring homomorphism on `R`.
|
RingEquiv.toMonoidHom_commutes
theorem RingEquiv.toMonoidHom_commutes :
∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R ≃+* S),
↑↑f = (↑f).toMonoidHom
This theorem, `RingEquiv.toMonoidHom_commutes`, states that for any two types `R` and `S`, both of which are non associative semirings, the two possible ways of coercing a ring equivalence `f` into a `MonoidHom` are equivalent. In other words, directly coercing `f` to a `MonoidHom` or first coercing `f` to a `RingHom` and then to a `MonoidHom` will yield the same result.
More concisely: For any non associative semirings R and S and a ring equivalence f : R ≅ S, the resulting MonoidHom's from directly coercing f or first coercing f to a RingHom then to a MonoidHom are equal.
|
RingEquiv.apply_symm_apply
theorem RingEquiv.apply_symm_apply :
∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S)
(x : S), e (e.symm x) = x
This theorem states that for any ring isomorphism `e` from a ring `R` to a ring `S`, and for any element `x` from `S`, applying the isomorphism `e` to the result of applying the inverse of `e` to `x` will yield `x` itself. In mathematical terms, for a ring isomorphism \(e: R \rightarrow S\), and any \(x \in S\), we have \(e(e^{-1}(x)) = x\). Essentially, this theorem is asserting the correctness of the inverse function of a ring isomorphism.
More concisely: For any ring isomorphism \(e: R \rightarrow S\), \(e \circ e^{-1} = id\_S\), where \(id\_S\) is the identity function on \(S\).
|
RingEquiv.bijective
theorem RingEquiv.bijective :
∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S),
Function.Bijective ⇑e
The theorem `RingEquiv.bijective` asserts that for any types `R` and `S` which both have multiplication (`Mul`) and addition (`Add`) operations defined on them, any ring isomorphism `e` (denoted as `R ≃+* S` in Lean) between `R` and `S` is a bijective function. In other words, the application of `e` (denoted as `⇑e`) is both injective (one-to-one) and surjective (onto).
More concisely: Given types `R` and `S` with multiplication and addition operations, and a ring isomorphism `e : R ≃+* S`, then `e` is a bijective function.
|
RingEquiv.symm_apply_apply
theorem RingEquiv.symm_apply_apply :
∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S)
(x : R), e.symm (e x) = x
The theorem `RingEquiv.symm_apply_apply` states that for all rings `R` and `S`, if we have a ring isomorphism `e` from `R` to `S`, then applying the isomorphism and its inverse in succession to any element `x` in `R` will recover the original element. In other words, the inverse of the isomorphism undoes the effect of the isomorphism, which is a fundamental property expected of any isomorphism. In mathematical terms, for any element `x` in `R`, `(RingEquiv.symm e) (e x) = x`.
More concisely: For any ring isomorphism `e` from `R` to `S`, `(RingEquiv.symm e) (e x) = x` for all `x` in `R`.
|
MulEquiv.noZeroDivisors
theorem MulEquiv.noZeroDivisors :
∀ {A : Type u_7} (B : Type u_8) [inst : MulZeroClass A] [inst_1 : MulZeroClass B] [inst_2 : NoZeroDivisors B],
A ≃* B → NoZeroDivisors A
The theorem `MulEquiv.noZeroDivisors` states that for any two types `A` and `B`, if `A` and `B` are both rings (with multiplication and zero), and `B` has the property that there are no zero divisors (meaning there are no non-zero elements `a` and `b` such that `a * b = 0`), then if `A` is isomorphic to `B` as a ring, `A` also has no zero divisors.
More concisely: If `A` and `B` are isomorphic ring structures with `B` having no zero divisors, then `A` also has no zero divisors.
|