# Theory More_Ring

theory More_Ring
imports Ring
```(*  Title:      HOL/Algebra/More_Ring.thy
*)

section ‹More on rings etc.›

theory More_Ring
imports
Ring
begin

lemma (in cring) field_intro2: "𝟬⇘R⇙ ~= 𝟭⇘R⇙ ⟹ ∀x ∈ carrier R - {𝟬⇘R⇙}. x ∈ Units R ⟹ field R"
apply (unfold_locales)
apply (insert cring_axioms, auto)
apply (rule trans)
apply (subgoal_tac "a = (a ⊗ b) ⊗ inv b")
apply assumption
apply (subst m_assoc)
apply auto
apply (unfold Units_def)
apply auto
done

lemma (in monoid) inv_char: "x : carrier G ⟹ y : carrier G ⟹
x ⊗ y = 𝟭 ⟹ y ⊗ x = 𝟭 ⟹ inv x = y"
apply (subgoal_tac "x : Units G")
apply (subgoal_tac "y = inv x ⊗ 𝟭")
apply simp
apply (erule subst)
apply (subst m_assoc [symmetric])
apply auto
apply (unfold Units_def)
apply auto
done

lemma (in comm_monoid) comm_inv_char: "x : carrier G ⟹ y : carrier G ⟹
x ⊗ y = 𝟭 ⟹ inv x = y"
apply (rule inv_char)
apply auto
apply (subst m_comm, auto)
done

lemma (in ring) inv_neg_one [simp]: "inv (⊖ 𝟭) = ⊖ 𝟭"
apply (rule inv_char)
apply (auto simp add: l_minus r_minus)
done

lemma (in monoid) inv_eq_imp_eq: "x : Units G ⟹ y : Units G ⟹
inv x = inv y ⟹ x = y"
apply (subgoal_tac "inv(inv x) = inv(inv y)")
apply (subst (asm) Units_inv_inv)+
apply auto
done

lemma (in ring) Units_minus_one_closed [intro]: "⊖ 𝟭 : Units R"
apply (unfold Units_def)
apply auto
apply (rule_tac x = "⊖ 𝟭" in bexI)
apply auto
done

lemma (in monoid) inv_one [simp]: "inv 𝟭 = 𝟭"
apply (rule inv_char)
apply auto
done

lemma (in ring) inv_eq_neg_one_eq: "x : Units R ⟹ (inv x = ⊖ 𝟭) = (x = ⊖ 𝟭)"
apply auto
apply (subst Units_inv_inv [symmetric])
apply auto
done

lemma (in monoid) inv_eq_one_eq: "x : Units G ⟹ (inv x = 𝟭) = (x = 𝟭)"
by (metis Units_inv_inv inv_one)

end
```