Theorems · Definition · commutative algebra

Algebra.IsEpi.casesOn

{R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          {motive : Algebra.IsEpi R A → Sort u} →
            (t : Algebra.IsEpi R A) →
              ((injective_lift_mul : Function.Injective ⇑(TensorProduct.lift (LinearMap.mul R A))) → motive ⋯) →
                motive t

Defined in

Mathlib.Algebra.Algebra.Epi

Cited by

0 results in Mathlib

Foundations

Depth 59 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringSemiringAlgebra