isCancelMulZero_iff_noZeroDivisors
theorem isCancelMulZero_iff_noZeroDivisors : ∀ (α : Type u_2) [inst : Ring α], IsCancelMulZero α ↔ NoZeroDivisors α
This theorem states that in any ring `α`, the properties of `IsCancelMulZero` and `NoZeroDivisors` are equivalent. The property `IsCancelMulZero` refers to the fact that if a product of two elements in the ring is zero, then one or both of the elements must be zero. `NoZeroDivisors` means that there are no two non-zero elements in the ring that multiply to zero. Thus, the theorem states that a ring has the `IsCancelMulZero` property if and only if it has the `NoZeroDivisors` property.
More concisely: In a ring, the absence of zero divisors is equivalent to every element being cancellable for multiplication with zero.
|
map_bit0
theorem map_bit0 :
∀ {α : Type u_2} {β : Type u_3} {F : Type u_4} [inst : NonAssocSemiring α] [inst_1 : NonAssocSemiring β]
[inst_2 : FunLike F α β] [inst_3 : AddHomClass F α β] (f : F) (a : α), f (bit0 a) = bit0 (f a)
The theorem `map_bit0` states that for any types `α`, `β`, and `F`, given that `α` and `β` are equipped with the structure of a non-associative semiring, `F` is a function-like object from `α` to `β`, and `F` additionally has the structure of an additive homomorphism class, then for any element `f` of type `F` and any element `a` of type `α`, mapping `f` to `bit0 a` (which is shorthand for adding `a` to itself in the semiring `α`) equals the `bit0` (i.e., the sum with itself in the semiring `β`) of the image of `a` under `f`. In other words, additive homomorphisms preserve the operation 'bit0', which essentially doubles a given element in a semiring.
More concisely: For any non-associative semirings `α` and `β`, additive homomorphism `F` from `α` to `β` satisfies `F(a) + F(a) = F(a + a)` for all `a` in `α`, where `+` denotes the semiring addition and `F(a + a)` is shorthand for `F(bit0 a)`.
|
vieta_formula_quadratic
theorem vieta_formula_quadratic :
∀ {α : Type u_2} [inst : NonUnitalCommRing α] {b c x : α},
x * x - b * x + c = 0 → ∃ y, y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c
This is a theorem stating Vieta's formula for a quadratic equation. It states that for any root `x` of a monic quadratic polynomial characterized by coefficients `b` and `c`, there exists another root `y` such that the sum of `x` and `y` is equal to `b` and the product of `x` and `y` is equal to `c`. More formally, if `x` is a root of the polynomial equation `x * x - b * x + c = 0`, there exists `y` such that `y` is also a root of this equation, `x + y = b`, and `x * y = c`. This holds for any type `α` that forms a non-unital commutative ring.
More concisely: Given a monic quadratic polynomial with roots `x` and `y` over a commutative ring `α`, `x` and `y` satisfy the relations `x + y = b` and `x * y = c`.
|
NoZeroDivisors.to_isDomain
theorem NoZeroDivisors.to_isDomain :
∀ (α : Type u_2) [inst : Ring α] [h : Nontrivial α] [inst_1 : NoZeroDivisors α], IsDomain α
This theorem states that for any type `α` that has a ring structure, is nontrivial, and has no zero divisors, `α` is a domain. In mathematical terminology, a ring `α` is a domain if it contains no zero divisors and is nontrivial (i.e., it has at least two distinct elements).
More concisely: A nontrivial ring without zero divisors is a domain.
|