Is there a mul_left_inj for rings..?

Stream: Is there code for X?

[Ben]

Looking for something like

lemma ring_mul_left_inj {R: Type} [ring R] (a: R) {b c: R} (h1: a ≠ 0) : b * a = c * a ↔ b = c := by sorry

I think I am correct because I have accounted for a being zero. Library search didn't reveal anything...?

[Ruben Van de Velde]

docs#mul_left_inj' ?

[Thomas Browning]

You need to assume that R has no zero divisors.

[Thomas Browning]

huh, is mathlib missing an instance?

instance inst {R : Type*} [hR : ring R] [no_zero_divisors R] : cancel_monoid_with_zero R :=
{ mul_zero := mul_zero,
  zero_mul := zero_mul,
  mul_left_cancel_of_ne_zero :=
  λ a b c ha h, by rwa [←sub_eq_zero, ←mul_sub, mul_eq_zero, sub_eq_zero, or_iff_right ha] at h,
  mul_right_cancel_of_ne_zero :=
  λ a b c hb h, by rwa [←sub_eq_zero, ←sub_mul, mul_eq_zero, sub_eq_zero, or_iff_left hb] at h,
  .. hR }

lemma ring_mul_left_inj {R : Type*} [ring R] [no_zero_divisors R] (a : R) {b c : R} (h1 : a ≠ 0) :
  b * a = c * a ↔ b = c :=
mul_left_inj' h1

[Thomas Browning]

Ah, docs#no_zero_divisors.to_cancel_monoid_with_zero is not an instance.

[Thomas Browning]

attribute [instance] no_zero_divisors.to_cancel_monoid_with_zero

lemma ring_mul_left_inj {R : Type*} [ring R] [no_zero_divisors R] (a : R) {b c : R} (h1 : a ≠ 0) :
  b * a = c * a ↔ b = c :=
mul_left_inj' h1

[Ben]

Ah okay I think I understand, apologies if this is going off the topic. But now getting that it can't find 1 in the target at rw ←is_hom.map_one...? Any ideas what is going wrong here...?

import algebra.field.defs
import algebra.group_with_zero.basic

class field_homomorphism {R S: Type} [field R] [field S] (func: R → S) :=
(map_add: ∀a b: R, func (a + b) = func a + func b)
(map_mul: ∀a b: R, func (a * b) = func a * func b)
(map_one: func 1 = 1)

def is_unit {R: Type} [field R] (a: R) : Prop := ∃b: R, a * b = 1
def unit_field (R: Type) [field R] : Type := @subtype R (is_unit)

example {R S: Type} [field R] [field S] (θ: R → S) (is_hom: field_homomorphism θ) (u: unit_field R) :
  (θ u.1)⁻¹ = (θ u.1⁻¹) := begin
  cases u,
  cases u_property with u_div u_divides,
  simp,
  rw ←mul_left_inj' one_ne_zero,
  rw ←is_hom.map_one,
  rw ←is_hom.map_mul (u_val⁻¹) (1: R),
  rw ←u_divides,
  rw ←mul_assoc,
  rw mul_comm (u_val⁻¹) _,
  rw mul_right_div,
  rw one_mul,
  rw u_divides,
  rw div_thing,
  rw ←is_hom.map_mul,
  rw mul_comm,
  rw u_divides,
end

[Thomas Browning]

I think the issue is that you aren't importing enough for mul_left_inj' to know that S is a cancel_monoid_with_zero.

[Thomas Browning]

But there are easier ways to prove this:

import algebra.field.defs
import algebra.group_with_zero.basic

variables {R S: Type*} [field R] [field S]

class field_homomorphism (func : R → S) :=
(map_add : ∀ a b : R, func (a + b) = func a + func b)
(map_mul : ∀ a b : R, func (a * b) = func a * func b)
(map_one : func 1 = 1)

lemma field_homomorphism.map_zero {θ : R → S} (is_hom : field_homomorphism θ) : θ 0 = 0 :=
by simpa using is_hom.map_add 0 0

example (θ : R → S) (is_hom : field_homomorphism θ) (u : R) : (θ u)⁻¹ = θ u⁻¹ :=
begin
  rcases eq_or_ne u 0 with rfl | h,
  { rw [inv_zero, is_hom.map_zero, inv_zero] },
  apply inv_eq_of_mul_eq_one_left,
  rw [←is_hom.map_mul, inv_mul_cancel h, is_hom.map_one],
end