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) 2014 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Yury Kudryashov, Neil Strickland
! This file was ported from Lean 3 source module algebra.ring.units
! leanprover-community/mathlib commit 2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Ring.InjSurj
import Mathlib.Algebra.Group.Units
/-!
# Units in semirings and rings
-/
universe u v w x
variable { α : Type u } { β : Type v } { γ : Type w } { R : Type x }
open Function
namespace Units
section HasDistribNeg
variable [ Monoid α ] [ HasDistribNeg : (α : Type ?u.1880) → [inst : Mul α Type ?u.1880 α ] { a b : α }
/-- Each element of the group of units of a ring has an additive inverse. -/
instance : Neg α ˣ :=
⟨ fun u => ⟨-↑ u , -↑ u ⁻¹, by simp , by simp ⟩⟩
/-- Representing an element of a ring's unit group as an element of the ring commutes with
mapping this element to its additive inverse. -/
@[ simp , norm_cast ]
protected theorem val_neg ( u : α ˣ) : (↑(- u ) : α ) = - u :=
rfl : ∀ {α : Sort ?u.2876} {a : α }, a = a
#align units.coe_neg Units.val_neg
@[ simp , norm_cast ]
protected theorem coe_neg_one : ((- 1 : α ˣ) : α ) = - 1 :=
rfl : ∀ {α : Sort ?u.3984} {a : α }, a = a
#align units.coe_neg_one Units.coe_neg_one
instance : HasDistribNeg : (α : Type ?u.4284) → [inst : Mul α Type ?u.4284 α ˣ :=
Units.ext . hasDistribNeg _ Units.val_neg Units.val_mul : ∀ {α : Type ?u.4904} [inst : Monoid α a b : α ˣ ↑(a * b = ↑a * ↑b
@[ field_simps ]
theorem neg_divp : ∀ (a : α ) (u : α ˣ - (a /ₚ u = - a /ₚ u neg_divp ( a : α ) ( u : α ˣ) : -( a /ₚ u ) = - a /ₚ u := by simp only [ divp : {α : Type ?u.5535} → [inst : Monoid α α → α ˣ α , neg_mul ]
#align units.neg_divp Units.neg_divp
end HasDistribNeg
section Ring
variable [ Ring α ] { a b : α }
-- Needs to have higher simp priority than divp_add_divp. 1000 is the default priority.
@[ field_simps 1010]
theorem divp_add_divp_same : ∀ {α : Type u} [inst : Ring α a b : α ) (u : α ˣ a /ₚ u + b /ₚ u = (a + b /ₚ u divp_add_divp_same ( a b : α ) ( u : α ˣ) : a /ₚ u + b /ₚ u = ( a + b ) /ₚ u := by
simp only [ divp : {α : Type ?u.6069} → [inst : Monoid α α → α ˣ α , add_mul ]
#align units.divp_add_divp_same Units.divp_add_divp_same : ∀ {α : Type u} [inst : Ring α a b : α ) (u : α ˣ a /ₚ u + b /ₚ u = (a + b /ₚ u
-- Needs to have higher simp priority than divp_sub_divp. 1000 is the default priority.
@[ field_simps 1010]
theorem divp_sub_divp_same : ∀ {α : Type u} [inst : Ring α a b : α ) (u : α ˣ a /ₚ u - b /ₚ u = (a - b /ₚ u divp_sub_divp_same ( a b : α ) ( u : α ˣ) : a /ₚ u - b /ₚ u = ( a - b ) /ₚ u := by
rw [ sub_eq_add_neg , sub_eq_add_neg , neg_divp , divp_add_divp_same : ∀ {α : Type ?u.6727} [inst : Ring α a b : α ) (u : α ˣ a /ₚ u + b /ₚ u = (a + b /ₚ u ]
#align units.divp_sub_divp_same Units.divp_sub_divp_same : ∀ {α : Type u} [inst : Ring α a b : α ) (u : α ˣ a /ₚ u - b /ₚ u = (a - b /ₚ u
@[ field_simps ]
theorem add_divp : ∀ {α : Type u} [inst : Ring α a b : α ) (u : α ˣ a + b /ₚ u = (a * ↑u + b /ₚ u add_divp ( a b : α ) ( u : α ˣ) : a + b /ₚ u = ( a * u + b ) /ₚ u := by
simp only [ divp : {α : Type ?u.7402} → [inst : Monoid α α → α ˣ α , add_mul , Units.mul_inv_cancel_right : ∀ {α : Type ?u.7436} [inst : Monoid α a : α ) (b : α ˣ a * ↑b * ↑b ⁻¹ = a ]
#align units.add_divp Units.add_divp : ∀ {α : Type u} [inst : Ring α a b : α ) (u : α ˣ a + b /ₚ u = (a * ↑u + b /ₚ u
@[ field_simps ]
theorem sub_divp : ∀ (a b : α ) (u : α ˣ a - b /ₚ u = (a * ↑u - b /ₚ u sub_divp ( a b : α ) ( u : α ˣ) : a - b /ₚ u = ( a * u - b ) /ₚ u := by
simp only [ divp : {α : Type ?u.8287} → [inst : Monoid α α → α ˣ α , sub_mul , Units.mul_inv_cancel_right : ∀ {α : Type ?u.8317} [inst : Monoid α a : α ) (b : α ˣ a * ↑b * ↑b ⁻¹ = a ]
#align units.sub_divp Units.sub_divp : ∀ {α : Type u} [inst : Ring α a b : α ) (u : α ˣ a - b /ₚ u = (a * ↑u - b /ₚ u
@[ field_simps ]
theorem divp_add : ∀ {α : Type u} [inst : Ring α a b : α ) (u : α ˣ a /ₚ u + b = (a + b * ↑u /ₚ u divp_add ( a b : α ) ( u : α ˣ) : a /ₚ u + b = ( a + b * u ) /ₚ u := by
simp only [ divp : {α : Type ?u.9156} → [inst : Monoid α α → α ˣ α , add_mul , Units.mul_inv_cancel_right : ∀ {α : Type ?u.9190} [inst : Monoid α a : α ) (b : α ˣ a * ↑b * ↑b ⁻¹ = a ]
#align units.divp_add Units.divp_add : ∀ {α : Type u} [inst : Ring α a b : α ) (u : α ˣ a /ₚ u + b = (a + b * ↑u /ₚ u
@[ field_simps ]
theorem divp_sub : ∀ (a b : α ) (u : α ˣ a /ₚ u - b = (a - b * ↑u /ₚ u divp_sub ( a b : α ) ( u : α ˣ) : a /ₚ u - b = ( a - b * u ) /ₚ u := by
simp only [ divp : {α : Type ?u.10037} → [inst : Monoid α α → α ˣ α , sub_mul , sub_right_inj : ∀ {G : Type ?u.10067} [inst : AddGroup G a b c : G }, a - b = a - c ↔ b = c ]
rw [ mul_assoc : ∀ {G : Type ?u.10319} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c , Units.mul_inv : ∀ {α : Type ?u.10475} [inst : Monoid α a : α ˣ ↑a * ↑a ⁻¹ = 1 , mul_one ]
#align units.divp_sub Units.divp_sub : ∀ {α : Type u} [inst : Ring α a b : α ) (u : α ˣ a /ₚ u - b = (a - b * ↑u /ₚ u
end Ring
end Units
theorem IsUnit.neg [ Monoid α ] [ HasDistribNeg : (α : Type ?u.10677) → [inst : Mul α Type ?u.10677 α ] { a : α } : IsUnit a → IsUnit (- a )
| ⟨ x , hx ⟩ => hx ▸ (- x ). isUnit
#align is_unit.neg IsUnit.neg
@[ simp ]
theorem IsUnit.neg_iff [ Monoid α ] [ HasDistribNeg : (α : Type ?u.11311) → [inst : Mul α Type ?u.11311 α ] ( a : α ) : IsUnit (- a ) ↔ IsUnit a :=
⟨ fun h => neg_neg a ▸ h . neg , IsUnit.neg ⟩
#align is_unit.neg_iff IsUnit.neg_iff
theorem IsUnit.sub_iff [ Ring α ] { x y : α } : IsUnit ( x - y ) ↔ IsUnit ( y - x ) :=
( IsUnit.neg_iff _ ). symm : ∀ {a b : Prop }, (a ↔ b b ↔ a symm . trans : ∀ {a b c : Prop }, (a ↔ b (b ↔ c a ↔ c trans <| neg_sub x y ▸ Iff.rfl : ∀ {a : Prop }, a ↔ a
#align is_unit.sub_iff IsUnit.sub_iff
namespace Units
@[ field_simps ]
theorem divp_add_divp : ∀ [inst : CommRing α a b : α ) (u₁ u₂ : α ˣ a /ₚ u₁ + b /ₚ u₂ = (a * ↑u₂ + ↑u₁ * b /ₚ (u₁ * u₂ divp_add_divp [ CommRing α ] ( a b : α ) ( u₁ u₂ : α ˣ) :
a /ₚ u₁ + b /ₚ u₂ = ( a * u₂ + u₁ * b ) /ₚ ( u₁ * u₂ ) := by
simp only [ divp : {α : Type ?u.13588} → [inst : Monoid α α → α ˣ α , add_mul , mul_inv_rev , val_mul : ∀ {α : Type ?u.13641} [inst : Monoid α a b : α ˣ ↑(a * b = ↑a * ↑b ]
rw [ mul_comm (↑ u₁ * b ), mul_comm b ]
rw [ ← mul_assoc : ∀ {G : Type ?u.14375} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c , ← mul_assoc : ∀ {G : Type ?u.14476} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c , mul_assoc : ∀ {G : Type ?u.14552} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c a , mul_assoc : ∀ {G : Type ?u.14563} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c (↑ u₂ ⁻¹ : α ), mul_inv , inv_mul , mul_one ,
mul_one ]
-- porting note: `assoc_rw` not ported: `assoc_rw [mul_inv, mul_inv, mul_one, mul_one]`
#align units.divp_add_divp Units.divp_add_divp : ∀ {α : Type u} [inst : CommRing α a b : α ) (u₁ u₂ : α ˣ a /ₚ u₁ + b /ₚ u₂ = (a * ↑u₂ + ↑u₁ * b /ₚ (u₁ * u₂
@[ field_simps ]
theorem divp_sub_divp : ∀ {α : Type u} [inst : CommRing α a b : α ) (u₁ u₂ : α ˣ a /ₚ u₁ - b /ₚ u₂ = (a * ↑u₂ - ↑u₁ * b /ₚ (u₁ * u₂ divp_sub_divp [ CommRing α ] ( a b : α ) ( u₁ u₂ : α ˣ) :
a /ₚ u₁ - b /ₚ u₂ = ( a * u₂ - u₁ * b ) /ₚ ( u₁ * u₂ ) := by
simp only [ sub_eq_add_neg , neg_divp , divp_add_divp : ∀ {α : Type ?u.16269} [inst : CommRing α a b : α ) (u₁ u₂ : α ˣ a /ₚ u₁ + b /ₚ u₂ = (a * ↑u₂ + ↑u₁ * b /ₚ (u₁ * u₂ , mul_neg ]
#align units.divp_sub_divp Units.divp_sub_divp : ∀ {α : Type u} [inst : CommRing α a b : α ) (u₁ u₂ : α ˣ a /ₚ u₁ - b /ₚ u₂ = (a * ↑u₂ - ↑u₁ * b /ₚ (u₁ * u₂
theorem add_eq_mul_one_add_div : ∀ [inst : Semiring R a : R ˣ b : R }, ↑a + b = ↑a * (1 + ↑a ⁻¹ * b add_eq_mul_one_add_div [ Semiring R ] { a : R ˣ} { b : R } : ↑ a + b = a * ( 1 + ↑ a ⁻¹ * b ) := by
rw [ mul_add , mul_one , ← mul_assoc : ∀ {G : Type ?u.18091} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c , Units.mul_inv : ∀ {α : Type ?u.18226} [inst : Monoid α a : α ˣ ↑a * ↑a ⁻¹ = 1 , one_mul ]
#align units.add_eq_mul_one_add_div Units.add_eq_mul_one_add_div : ∀ {R : Type x} [inst : Semiring R a : R ˣ b : R }, ↑a + b = ↑a * (1 + ↑a ⁻¹ * b
end Units