Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2019 Kenny Lau. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kenny Lau
! This file was ported from Lean 3 source module algebra.punit_instances
! leanprover-community/mathlib commit 6cb77a8eaff0ddd100e87b1591c6d3ad319514ff
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Module.Basic
import Mathlib.Algebra.GCDMonoid.Basic
import Mathlib.Algebra.GroupRingAction.Basic
import Mathlib.GroupTheory.GroupAction.Defs
import Mathlib.Order.CompleteBooleanAlgebra
/-!
# Instances on PUnit
This file collects facts about algebraic structures on the one-element type, e.g. that it is a
commutative ring.
-/
namespace PUnit
@[ to_additive ]
instance commGroup : CommGroup PUnit where
mul _ _ := unit
one := unit
inv _ := unit
div _ _ := unit
npow _ _ := unit
zpow _ _ := unit
mul_assoc := by intros a✝ * b✝ * c✝ = a✝ * (b✝ * c✝ ; a✝ * b✝ * c✝ = a✝ * (b✝ * c✝ rfl
one_mul := by intros ; rfl
mul_one := by intros ; rfl
mul_left_inv := by intros ; rfl
mul_comm := by intros ; rfl
-- shortcut instances
@[ to_additive ] instance : One PUnit where one := ()
@[ to_additive ] instance : Mul PUnit where mul _ _ := ()
@[ to_additive ] instance : Div PUnit where div _ _ := ()
@[ to_additive ] instance : Inv PUnit where inv _ := ()
@[ to_additive ( attr := simp )]
theorem one_eq : ( 1 : PUnit ) = unit :=
rfl : ∀ {α : Sort ?u.1430} {a : α }, a = a
#align punit.one_eq PUnit.one_eq
#align punit.zero_eq PUnit.zero_eq
@[ to_additive ( attr := simp )]
theorem mul_eq : x * y = unit :=
rfl : ∀ {α : Sort ?u.1518} {a : α }, a = a
#align punit.mul_eq PUnit.mul_eq
#align punit.add_eq PUnit.add_eq
-- `sub_eq` simplifies `PUnit.sub_eq`, but the latter is eligible for `dsimp`
@[ to_additive ( attr := simp , nolint simpNF )]
theorem div_eq : x / y = unit :=
rfl : ∀ {α : Sort ?u.1625} {a : α }, a = a
#align punit.div_eq PUnit.div_eq
#align punit.sub_eq PUnit.sub_eq
-- `neg_eq` simplifies `PUnit.neg_eq`, but the latter is eligible for `dsimp`
@[ to_additive ( attr := simp , nolint simpNF )]
theorem inv_eq : x ⁻¹ = unit :=
rfl : ∀ {α : Sort ?u.1787} {a : α }, a = a
#align punit.inv_eq PUnit.inv_eq
#align punit.neg_eq PUnit.neg_eq
instance commRing : CommRing PUnit where
__ := PUnit.commGroup
__ := PUnit.addCommGroup
left_distrib := by intros a✝ * (b✝ + c✝ = a✝ * b✝ + a✝ * c✝ ; a✝ * (b✝ + c✝ = a✝ * b✝ + a✝ * c✝ rfl
right_distrib := by intros (a✝ + b✝ * c✝ = a✝ * c✝ + b✝ * c✝ ; (a✝ + b✝ * c✝ = a✝ * c✝ + b✝ * c✝ rfl
zero_mul := by intros ; rfl
mul_zero := by intros ; rfl
natCast _ := unit
instance cancelCommMonoidWithZero : CancelCommMonoidWithZero : Type ?u.3220 → Type ?u.3220 PUnit := by
refine' { PUnit.commRing with .. } ; intros ; exact Subsingleton.elim _ _
instance normalizedGCDMonoid : NormalizedGCDMonoid PUnit where
gcd _ _ := unit
lcm _ _ := unit
normUnit _ := 1
normUnit_zero := rfl : ∀ {α : Sort ?u.4412} {a : α }, a = a
normUnit_mul := by
∀ {a b : PUnit }, a ≠ 0 b ≠ 0 (fun x => 1 ) (a * b = (fun x => 1 ) a * (fun x => 1 ) b intros a✝², b✝ : PUnit a✝¹ : a✝² ≠ 0 a✝ : b✝ ≠ 0 (fun x => 1 ) (a✝² * b✝ = (fun x => 1 ) a✝² * (fun x => 1 ) b✝ ; a✝², b✝ : PUnit a✝¹ : a✝² ≠ 0 a✝ : b✝ ≠ 0 (fun x => 1 ) (a✝² * b✝ = (fun x => 1 ) a✝² * (fun x => 1 ) b✝
∀ {a b : PUnit }, a ≠ 0 b ≠ 0 (fun x => 1 ) (a * b = (fun x => 1 ) a * (fun x => 1 ) b rfl
normUnit_coe_units := by intros ; rfl
gcd_dvd_left _ _ := ⟨ unit , Subsingleton.elim _ _ ⟩
gcd_dvd_right _ _ := ⟨ unit , Subsingleton.elim _ _ ⟩
dvd_gcd { _ _ } _ _ _ := ⟨ unit , Subsingleton.elim _ _ ⟩
gcd_mul_lcm _ _ := ⟨ 1 , Subsingleton.elim _ _ ⟩
lcm_zero_left := by intros (fun x x => unit ) 0 a✝ = 0 ; (fun x x => unit ) 0 a✝ = 0 rfl
lcm_zero_right := by intros (fun x x => unit ) a✝ 0 = 0 ; (fun x x => unit ) a✝ 0 = 0 rfl
normalize_gcd := by intros ; rfl
normalize_lcm := by intros ; rfl
--porting notes: simpNF lint: simp can prove this @[simp]
theorem gcd_eq : gcd x y = unit :=
rfl : ∀ {α : Sort ?u.5511} {a : α }, a = a
#align punit.gcd_eq PUnit.gcd_eq
--porting notes: simpNF lint: simp can prove this @[simp]
theorem lcm_eq : lcm x y = unit :=
rfl : ∀ {α : Sort ?u.5615} {a : α }, a = a
#align punit.lcm_eq PUnit.lcm_eq
@[ simp ]
theorem norm_unit_eq { x : PUnit } : normUnit x = 1 :=
rfl : ∀ {α : Sort ?u.6113} {a : α }, a = a
#align punit.norm_unit_eq PUnit.norm_unit_eq
instance canonicallyOrderedAddMonoid : CanonicallyOrderedAddMonoid : Type ?u.6127 → Type ?u.6127 PUnit := by
refine'
{ PUnit.commRing , PUnit.completeBooleanAlgebra with
exists_add_of_le := fun { _ _ } _ => ⟨ unit , Subsingleton.elim _ _ ⟩.. } <;>
intros <;>
trivial
instance linearOrderedCancelAddCommMonoid : LinearOrderedCancelAddCommMonoid : Type ?u.7192 → Type ?u.7192 PUnit where
__ := PUnit.canonicallyOrderedAddMonoid
__ := PUnit.linearOrder
le_of_add_le_add_left _ _ _ _ := trivial
add_le_add_left := by intros ; rfl
instance : LinearOrderedAddCommMonoidWithTop : Type ?u.8225 → Type ?u.8225 PUnit :=
{ PUnit.completeBooleanAlgebra , PUnit.linearOrderedCancelAddCommMonoid with
top_add' := fun _ => rfl : ∀ {α : Sort ?u.8396} {a : α }, a = a }
@[ to_additive ]
instance smul : SMul : Type ?u.9201 → Type ?u.9200 → Type (max?u.9201?u.9200) R PUnit :=
⟨ fun _ _ => unit ⟩
@[ to_additive ( attr := simp )]
theorem smul_eq { R : Type _ } ( y : PUnit ) ( r : R ) : r • y = unit :=
rfl : ∀ {α : Sort ?u.9405} {a : α }, a = a
#align punit.smul_eq PUnit.smul_eq
#align punit.vadd_eq PUnit.vadd_eq
@[ to_additive ]
instance : IsCentralScalar R PUnit :=
⟨ fun _ _ => rfl : ∀ {α : Sort ?u.9572} {a : α }, a = a ⟩
@[ to_additive ]
instance : SMulCommClass : (M : Type ?u.9653) → (N : Type ?u.9652) → (α : Type ?u.9651) → [inst : SMul M α [inst : SMul N α Prop R S PUnit :=
⟨ fun _ _ _ => rfl : ∀ {α : Sort ?u.9788} {a : α }, a = a ⟩
@[ to_additive ]
instance [ SMul : Type ?u.9884 → Type ?u.9883 → Type (max?u.9884?u.9883) R S ] : IsScalarTower : (M : Type ?u.9889) →
(N : Type ?u.9888) → (α : Type ?u.9887) → [inst : SMul M N [inst : SMul N α [inst : SMul M α Prop R S PUnit :=
⟨ fun _ _ _ => rfl : ∀ {α : Sort ?u.10065} {a : α }, a = a ⟩
instance smulWithZero [ Zero R ] : SMulWithZero : (R : Type ?u.10184) → (M : Type ?u.10183) → [inst : Zero R [inst : Zero M Type (max?u.10184?u.10183) R PUnit := by
refine' { PUnit.smul with .. } <;> intros <;> exact Subsingleton.elim _ _
instance mulAction [ Monoid R ] : MulAction : (α : Type ?u.10478) → Type ?u.10477 → [inst : Monoid α Type (max?u.10478?u.10477) R PUnit := by
refine' { PUnit.smul with .. } : MulAction ?m.10501 ?m.10502 PUnit.smul { PUnit.smul with .. } : MulAction ?m.10501 ?m.10502 { PUnit.smul with .. } : MulAction ?m.10501 ?m.10502 with { PUnit.smul with .. } : MulAction ?m.10501 ?m.10502 <;> intros refine'_2 (x✝ * y✝ • b✝ = x✝ • y✝ • b✝ <;> refine'_1 refine'_2 (x✝ * y✝ • b✝ = x✝ • y✝ • b✝ exact Subsingleton.elim _ _
instance distribMulAction [ Monoid R ] : DistribMulAction R PUnit := by
refine' { PUnit.mulAction with .. } <;> intros refine'_2 a✝ • (x✝ + y✝ = a✝ • x✝ + a✝ • y✝ <;> refine'_1 refine'_2 a✝ • (x✝ + y✝ = a✝ • x✝ + a✝ • y✝ exact Subsingleton.elim _ _
instance mulDistribMulAction [ Monoid R ] : MulDistribMulAction : (M : Type ?u.11244) → (A : Type ?u.11243) → [inst : Monoid M [inst : Monoid A Type (max?u.11244?u.11243) R PUnit := by
refine' { PUnit.mulAction with .. } <;> intros refine'_1 r✝ • (x✝ * y✝ = r✝ • x✝ * r✝ • y✝ <;> refine'_1 r✝ • (x✝ * y✝ = r✝ • x✝ * r✝ • y✝ refine'_2 exact Subsingleton.elim _ _
instance mulSemiringAction [ Semiring R ] : MulSemiringAction : (M : Type ?u.11914) → (R : Type ?u.11913) → [inst : Monoid M [inst : Semiring R Type (max?u.11914?u.11913) R PUnit :=
{ PUnit.distribMulAction, PUnit.mulDistribMulAction with } : MulSemiringAction ?m.12217 ?m.12218 PUnit.distribMulAction { PUnit.distribMulAction, PUnit.mulDistribMulAction with } : MulSemiringAction ?m.12217 ?m.12218 PUnit.mulDistribMulAction { PUnit.distribMulAction, PUnit.mulDistribMulAction with } : MulSemiringAction ?m.12217 ?m.12218 { PUnit.distribMulAction, PUnit.mulDistribMulAction with } : MulSemiringAction ?m.12217 ?m.12218 with { PUnit.distribMulAction, PUnit.mulDistribMulAction with } : MulSemiringAction ?m.12217 ?m.12218
instance mulActionWithZero [ MonoidWithZero : Type ?u.13015 → Type ?u.13015 R ] : MulActionWithZero R PUnit :=
{ PUnit.mulAction , PUnit.smulWithZero with }
instance module [ Semiring R ] : Module R PUnit := by
refine' { PUnit.distribMulAction with .. } : Module ?m.13911 ?m.13912 PUnit.distribMulAction { PUnit.distribMulAction with .. } : Module ?m.13911 ?m.13912 { PUnit.distribMulAction with .. } : Module ?m.13911 ?m.13912 with { PUnit.distribMulAction with .. } : Module ?m.13911 ?m.13912 <;> intros <;> refine'_1 (r✝ + s✝ • x✝ = r✝ • x✝ + s✝ • x✝ refine'_2 exact Subsingleton.elim _ _
end PUnit