Commit 2023-02-19 01:12 1666fe00

View on Github →

feat: port Algebra.Algebra.Basic (#2244)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Algebra/Basic.lean

added def Algebra.algebraMapSubmonoid

added theorem Algebra.algebraMap_eq_smul_one'

added theorem Algebra.algebraMap_eq_smul_one

added theorem Algebra.algebraMap_ofSubring

added theorem Algebra.algebraMap_ofSubring_apply

added theorem Algebra.algebraMap_ofSubsemiring

added theorem Algebra.algebraMap_ofSubsemiring_apply

added theorem Algebra.algebraMap_pUnit

added theorem Algebra.algebra_ext

added def Algebra.cast

added theorem Algebra.coe_algebraMap_ofSubring

added theorem Algebra.coe_algebraMap_ofSubsemiring

added theorem Algebra.coe_linearMap

added theorem Algebra.commutes

added theorem Algebra.id.map_eq_id

added theorem Algebra.id.map_eq_self

added theorem Algebra.id.smul_eq_mul

added theorem Algebra.left_comm

added theorem Algebra.linearMap_apply

added theorem Algebra.mem_algebraMapSubmonoid_of_mem

added theorem Algebra.mul_sub_algebraMap_commutes

added theorem Algebra.mul_sub_algebraMap_pow_commutes

added def Algebra.ofModule'

added def Algebra.ofModule

added theorem Algebra.right_comm

added def Algebra.semiringToRing

added theorem Algebra.smul_def

added theorem LinearMap.ker_restrictScalars

added def LinearMap.ltoFun

added theorem LinearMap.map_algebraMap_mul

added theorem LinearMap.map_mul_algebraMap

added theorem Module.End_algebraMap_isUnit_inv_apply_eq_iff'

added theorem Module.End_algebraMap_isUnit_inv_apply_eq_iff

added theorem Module.End_isUnit_apply_inv_apply_of_isUnit

added theorem Module.End_isUnit_iff

added theorem Module.End_isUnit_inv_apply_apply_of_isUnit

added theorem Module.algebraMap_end_apply

added theorem Module.algebraMap_end_eq_smul_id

added theorem Module.ker_algebraMap_end

added theorem MulOpposite.algebraMap_apply

added theorem NeZero.of_noZeroSMulDivisors

added theorem NoZeroSMulDivisors.algebraMap_injective

added theorem NoZeroSMulDivisors.iff_algebraMap_injective

added theorem NoZeroSMulDivisors.of_algebraMap_injective

added theorem NoZeroSMulDivisors.trans

added theorem Rat.smul_one_eq_coe

added theorem RingHom.algebraMap_toAlgebra

added theorem RingHom.map_rat_algebraMap

added def RingHom.toAlgebra'

added def RingHom.toAlgebra

added theorem ULift.algebraMap_eq

added theorem ULift.down_algebraMap

added theorem algebraMap.coe_add

added theorem algebraMap.coe_div

added theorem algebraMap.coe_inj

added theorem algebraMap.coe_inv

added theorem algebraMap.coe_mul

added theorem algebraMap.coe_neg

added theorem algebraMap.coe_one

added theorem algebraMap.coe_pow

added theorem algebraMap.coe_prod

added theorem algebraMap.coe_rat_cast

added theorem algebraMap.coe_sum

added theorem algebraMap.coe_zero

added theorem algebraMap.coe_zpow

added theorem algebraMap.lift_map_eq_zero_iff

added def algebraMap

added theorem algebraMap_int_eq

added theorem algebraMap_rat_rat

added theorem algebraMap_smul

added theorem algebra_compatible_smul

added theorem int_cast_smul

added theorem smul_algebraMap

added theorem smul_algebra_smul_comm

Modified Mathlib/Algebra/Module/LinearMap.lean

modified theorem LinearMap.coe_restrictScalars

modified def LinearMap.restrictScalars