<commit_before>/-
Copyright (c) 2014 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>

Structures with multiplicative and additive components, including division rings and fields.
The development is modeled after Isabelle's library.

Ported from the standard library
-/
import algebra.ring
open core

namespace algebra

variable {A : Type}

-- in division rings, 1 / 0 = 0
structure division_ring [class] (A : Type) extends ring A, has_inv A, zero_ne_one_class A :=
  (mul_inv_cancel : Π{a}, a ≠ zero → mul a (inv a) = one)
  (inv_mul_cancel : Π{a}, a ≠ zero → mul (inv a) a = one)
  --(inv_zero : inv zero = zero)

section division_ring
  variables [s : division_ring A] {a b c : A}
  include s

  definition divide (a b : A) : A := a * b⁻¹
  infix `/` := divide

  -- only in this file
  local attribute divide [reducible]

  definition mul_inv_cancel (H : a ≠ 0) : a * a⁻¹ = 1 :=
  division_ring.mul_inv_cancel H

  definition inv_mul_cancel (H : a ≠ 0) : a⁻¹ * a = 1 :=
  division_ring.inv_mul_cancel H

  definition inv_eq_one_div : a⁻¹ = 1 / a := !one_mul⁻¹

-- the following are only theorems if we assume inv_zero here
/-  definition inv_zero : 0⁻¹ = 0 := !division_ring.inv_zero

  definition one_div_zero : 1 / 0 = 0 :=
    calc
      1 / 0 = 1 * 0⁻¹ : refl
        ... = 1 * 0 : division_ring.inv_zero A
        ... = 0 : mul_zero
-/

  definition div_eq_mul_one_div : a / b = a * (1 / b) :=
    by rewrite [↑divide, one_mul]

--  definition div_zero : a / 0 = 0 := by rewrite [div_eq_mul_one_div, one_div_zero, mul_zero]

  definition mul_one_div_cancel (H : a ≠ 0) : a * (1 / a) = 1 :=
    by rewrite [-inv_eq_one_div, (mul_inv_cancel H)]

  definition one_div_mul_cancel (H : a ≠ 0) : (1 / a) * a = 1 :=
    by rewrite [-inv_eq_one_div, (inv_mul_cancel H)]

  definition div_self (H : a ≠ 0) : a / a = 1 := mul_inv_cancel H

  definition one_div_one : 1 / 1 = (1:A) :=
  div_self (ne.symm zero_ne_one)

  definition mul_div_assoc : (a * b) / c = a * (b / c) := !mul.assoc

  definition one_div_ne_zero (H : a ≠ 0) : 1 / a ≠ 0 :=
    assume H2 : 1 / a = 0,
    have C1 : 0 = (1:A), from inverse (by rewrite [-(mul_one_div_cancel H), H2, mul_zero]),
    absurd C1 zero_ne_one

--  definition ne_zero_of_one_div_ne_zero (H : 1 / a ≠ 0) : a ≠ 0 :=
--    assume Ha : a = 0, absurd (Ha⁻¹ ▸ one_div_zero) H

  definition inv_one_eq : 1⁻¹ = (1:A) :=
    by rewrite [-mul_one, (inv_mul_cancel (ne.symm zero_ne_one))]

  definition div_one : a / 1 = a :=
    by rewrite [↑divide, inv_one_eq, mul_one]

  definition zero_div : 0 / a = 0 := !zero_mul

  -- note: integral domain has a "mul_ne_zero". Discrete fields are int domains.
  definition mul_ne_zero' (Ha : a ≠ 0) (Hb : b ≠ 0) : a * b ≠ 0 :=
    assume H : a * b = 0,
    have C1 : a = 0, by rewrite [-mul_one, -(mul_one_div_cancel Hb), -mul.assoc, H, zero_mul],
      absurd C1 Ha
<commit_msg>refactor(hott/algebra/field): cleanup<commit_after>/-
Copyright (c) 2014 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>

Structures with multiplicative and additive components, including division rings and fields.
The development is modeled after Isabelle's library.

Ported from the standard library
-/
import algebra.ring
open core

namespace algebra

variable {A : Type}

-- in division rings, 1 / 0 = 0
structure division_ring [class] (A : Type) extends ring A, has_inv A, zero_ne_one_class A :=
  (mul_inv_cancel : Π{a}, a ≠ zero → mul a (inv a) = one)
  (inv_mul_cancel : Π{a}, a ≠ zero → mul (inv a) a = one)
  --(inv_zero : inv zero = zero)

section division_ring
  variables [s : division_ring A] {a b c : A}
  include s

  definition divide (a b : A) : A := a * b⁻¹
  infix `/` := divide

  -- only in this file
  local attribute divide [reducible]

  definition mul_inv_cancel (H : a ≠ 0) : a * a⁻¹ = 1 :=
  division_ring.mul_inv_cancel H

  definition inv_mul_cancel (H : a ≠ 0) : a⁻¹ * a = 1 :=
  division_ring.inv_mul_cancel H

  definition inv_eq_one_div : a⁻¹ = 1 / a := !one_mul⁻¹

-- the following are only theorems if we assume inv_zero here
/-  definition inv_zero : 0⁻¹ = 0 := !division_ring.inv_zero

  definition one_div_zero : 1 / 0 = 0 :=
    calc
      1 / 0 = 1 * 0⁻¹ : refl
        ... = 1 * 0 : division_ring.inv_zero A
        ... = 0 : mul_zero
-/

  definition div_eq_mul_one_div : a / b = a * (1 / b) :=
    by rewrite [↑divide, one_mul]

--  definition div_zero : a / 0 = 0 := by rewrite [div_eq_mul_one_div, one_div_zero, mul_zero]

  definition mul_one_div_cancel (H : a ≠ 0) : a * (1 / a) = 1 :=
    by rewrite [-inv_eq_one_div, (mul_inv_cancel H)]

  definition one_div_mul_cancel (H : a ≠ 0) : (1 / a) * a = 1 :=
    by rewrite [-inv_eq_one_div, (inv_mul_cancel H)]

  definition div_self (H : a ≠ 0) : a / a = 1 := mul_inv_cancel H

  definition one_div_one : 1 / 1 = (1:A) :=
  div_self (ne.symm zero_ne_one)

  definition mul_div_assoc : (a * b) / c = a * (b / c) := !mul.assoc

  definition one_div_ne_zero (H : a ≠ 0) : 1 / a ≠ 0 :=
    assume H2 : 1 / a = 0,
    have C1 : 0 = (1:A), from inverse (by rewrite [-(mul_one_div_cancel H), H2, mul_zero]),
    absurd C1 zero_ne_one

--  definition ne_zero_of_one_div_ne_zero (H : 1 / a ≠ 0) : a ≠ 0 :=
--    assume Ha : a = 0, absurd (Ha⁻¹ ▸ one_div_zero) H

  definition inv_one_eq : 1⁻¹ = (1:A) :=
    by rewrite [-mul_one, (inv_mul_cancel (ne.symm (@zero_ne_one A _)))]

  definition div_one : a / 1 = a :=
    by rewrite [↑divide, inv_one_eq, mul_one]

  definition zero_div : 0 / a = 0 := !zero_mul

  -- note: integral domain has a "mul_ne_zero". Discrete fields are int domains.
  definition mul_ne_zero' (Ha : a ≠ 0) (Hb : b ≠ 0) : a * b ≠ 0 :=
    assume H : a * b = 0,
    have C1 : a = 0, by rewrite [-mul_one, -(mul_one_div_cancel Hb), -mul.assoc, H, zero_mul],
      absurd C1 Ha

{'fraction_non_alphanumeric': 0.1285154252599284, 'fraction_numerical': 0.02283961138571672, 'mean_word_length': 2.8758256274768823, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2325698', 'n_tokens_mistral': 2433, 'n_tokens_neox': 2239, 'n_words': 774}