Equiv.nontrivial
theorem Equiv.nontrivial : ∀ {α : Type u} {β : Type v}, α ≃ β → ∀ [inst : Nontrivial β], Nontrivial α
This theorem states that the property of being "nontrivial" can be transferred across an equivalence (`Equiv`) between two types. In other words, if there exists an equivalence between two types `α` and `β`, and if `β` is nontrivial (i.e., it has at least two distinct elements), then `α` must also be nontrivial.
More concisely: If `α` is equivalent to a nontrivial type `β`, then `α` is also a nontrivial type.
|
Finite.exists_type_zero_nonempty_mulEquiv
theorem Finite.exists_type_zero_nonempty_mulEquiv :
∀ (G : Type u) [inst : Group G] [inst_1 : Finite G], ∃ G' x x_1, Nonempty (G ≃* G')
This theorem states that for any finite group `G` in an arbitrary universe `u`, there exists an equivalent finite group `G'` in universe `0`, along with elements `x` and `x_1`. Here, equivalence is defined in terms of an isomorphism of groups, as given by the `G ≃* G'` notation, meaning that the group structures of `G` and `G'` are essentially the same.
More concisely: For any finite group `G` in an arbitrary universe `u`, there exists a finite group `G'` in universe `0` and isomorphisms `G ≃* G'` along with elements `x : G` and `x_1 : G'` such that `x` and `x_1` are mapped to each other under the isomorphisms.
|
Equiv.isDomain
theorem Equiv.isDomain :
∀ {α : Type u} {β : Type v} [inst : Ring α] [inst_1 : Ring β] [inst_2 : IsDomain β], α ≃+* β → IsDomain α := by
sorry
This theorem, `Equiv.isDomain`, states that for any two types `α` and `β`, if both `α` and `β` are rings, and `β` is an integral domain, then if there exists a ring isomorphism between `α` and `β`, `α` must also be an integral domain. In terms of mathematics, for any two rings A and B, if B is an integral domain (a nonzero commutative ring in which the product of any two nonzero elements is also nonzero), and there is an isomorphic mapping between A and B, then A is also an integral domain.
More concisely: If `α` and `β` are rings with `β` being an integral domain, and there exists a ring isomorphism between them, then `α` is also an integral domain.
|